equal
deleted
inserted
replaced
120 done |
120 done |
121 |
121 |
122 lemma inv_inv_aux: "5 \<le> p ==> |
122 lemma inv_inv_aux: "5 \<le> p ==> |
123 nat (p - 2) * nat (p - 2) = Suc (nat (p - 1) * nat (p - 3))" |
123 nat (p - 2) * nat (p - 2) = Suc (nat (p - 1) * nat (p - 3))" |
124 apply (subst int_int_eq [symmetric]) |
124 apply (subst int_int_eq [symmetric]) |
125 apply (simp add: zmult_int [symmetric]) |
125 apply (simp add: of_nat_mult) |
126 apply (simp add: left_diff_distrib right_diff_distrib) |
126 apply (simp add: left_diff_distrib right_diff_distrib) |
127 done |
127 done |
128 |
128 |
129 lemma zcong_zpower_zmult: |
129 lemma zcong_zpower_zmult: |
130 "[x^y = 1] (mod p) \<Longrightarrow> [x^(y * z) = 1] (mod p)" |
130 "[x^y = 1] (mod p) \<Longrightarrow> [x^(y * z) = 1] (mod p)" |