src/HOL/Number_Theory/Residues.thy
changeset 55227 653de351d21c
parent 55172 92735f0d5302
child 55242 413ec965f95d
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Fri Jan 31 19:32:13 2014 +0100
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Sat Feb 01 00:32:32 2014 +0000
     1.3 @@ -372,6 +372,12 @@
     1.4    finally show ?thesis .
     1.5  qed
     1.6  
     1.7 +lemma fermat_theorem_nat:
     1.8 +  assumes "prime p" and "~ (p dvd a)"
     1.9 +  shows "[a^(p - 1) = 1] (mod p)"
    1.10 +using fermat_theorem [of p a] assms
    1.11 +by (metis int_1 nat_int of_nat_power prime_int_def transfer_int_nat_cong zdvd_int)
    1.12 +
    1.13  
    1.14  subsection {* Wilson's theorem *}
    1.15