equal
deleted
inserted
replaced
363 apply (subst res_prime_units_eq) |
363 apply (subst res_prime_units_eq) |
364 apply (simp add: int_prod zmod_int prod_int_eq) |
364 apply (simp add: int_prod zmod_int prod_int_eq) |
365 done |
365 done |
366 finally have "fact (p - 1) mod p = \<ominus> \<one>" . |
366 finally have "fact (p - 1) mod p = \<ominus> \<one>" . |
367 then show ?thesis |
367 then show ?thesis |
368 by (metis of_nat_fact Divides.transfer_int_nat_functions(2) |
368 by (simp add: cong_int_def res_neg_eq res_one_eq zmod_int) |
369 cong_int_def res_neg_eq res_one_eq) |
|
370 qed |
369 qed |
371 |
370 |
372 lemma wilson_theorem: |
371 lemma wilson_theorem: |
373 assumes "prime p" |
372 assumes "prime p" |
374 shows "[fact (p - 1) = - 1] (mod p)" |
373 shows "[fact (p - 1) = - 1] (mod p)" |