version of Fermat's Theorem for type nat
authorpaulson <lp15@cam.ac.uk>
Sat Feb 01 00:32:32 2014 +0000 (2014-02-01)
changeset 55227653de351d21c
parent 55226 46c8969a995b
child 55228 901a6696cdd8
version of Fermat's Theorem for type nat
src/HOL/Number_Theory/Residues.thy
     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