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: