src/HOL/Number_Theory/Residues.thy
 changeset 59730 b7c394c7a619 parent 59667 651ea265d568 child 60526 fad653acf58f
```     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Tue Mar 10 16:12:35 2015 +0000
1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Mon Mar 16 15:30:00 2015 +0000
1.3 @@ -384,7 +384,7 @@
1.4
1.5  lemma (in residues_prime) wilson_theorem1:
1.6    assumes a: "p > 2"
1.7 -  shows "[fact (p - 1) = - 1] (mod p)"
1.8 +  shows "[fact (p - 1) = (-1::int)] (mod p)"
1.9  proof -
1.10    let ?InversePairs = "{ {x, inv x} | x. x : Units R - {\<one>, \<ominus> \<one>}}"
1.11    have UR: "Units R = {\<one>, \<ominus> \<one>} Un (Union ?InversePairs)"
1.12 @@ -430,9 +430,9 @@
1.13      apply (subst res_prime_units_eq)
1.14      apply (simp add: int_setprod zmod_int setprod_int_eq)
1.15      done
1.16 -  finally have "fact (p - 1) mod p = \<ominus> \<one>".
1.17 -  then show ?thesis
1.18 -    by (metis Divides.transfer_int_nat_functions(2) cong_int_def res_neg_eq res_one_eq)
1.19 +  finally have "fact (p - 1) mod p = (\<ominus> \<one> :: int)".
1.20 +  then show ?thesis
1.21 +    by (metis of_nat_fact Divides.transfer_int_nat_functions(2) cong_int_def res_neg_eq res_one_eq)
1.22  qed
1.23
1.24  lemma wilson_theorem:
```