equal
deleted
inserted
replaced
73 done |
73 done |
74 |
74 |
75 lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)" |
75 lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)" |
76 -- {* same as @{text WilsonRuss} *} |
76 -- {* same as @{text WilsonRuss} *} |
77 apply (unfold zcong_def) |
77 apply (unfold zcong_def) |
78 apply (simp add: Ring_and_Field.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2) |
78 apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2) |
79 apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans) |
79 apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans) |
80 apply (simp add: mult_commute) |
80 apply (simp add: mult_commute) |
81 apply (subst zdvd_zminus_iff) |
81 apply (subst zdvd_zminus_iff) |
82 apply (subst zdvd_reduce) |
82 apply (subst zdvd_reduce) |
83 apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans) |
83 apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans) |