src/HOL/Number_Theory/Residues.thy
changeset 59667 651ea265d568
parent 58889 5b7a9633cfa8
child 59730 b7c394c7a619
--- a/src/HOL/Number_Theory/Residues.thy	Tue Mar 10 11:56:32 2015 +0100
+++ b/src/HOL/Number_Theory/Residues.thy	Tue Mar 10 15:20:40 2015 +0000
@@ -8,10 +8,7 @@
 section {* Residue rings *}
 
 theory Residues
-imports
-  UniqueFactorization
-  Binomial
-  MiscAlgebra
+imports UniqueFactorization MiscAlgebra
 begin
 
 (*
@@ -275,15 +272,15 @@
   then have cop: "\<And>x. x \<in> {1::nat..p - 1} \<Longrightarrow> coprime x p"
     by blast
   { fix x::nat assume *: "1 < x" "x < p" and "x dvd p"
-    have "coprime x p" 
+    have "coprime x p"
       apply (rule cop)
       using * apply auto
       done
     with `x dvd p` `1 < x` have "False" by auto }
-  then show ?thesis 
-    using `2 \<le> p` 
+  then show ?thesis
+    using `2 \<le> p`
     by (simp add: prime_def)
-       (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0 
+       (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0
               not_numeral_le_zero one_dvd)
 qed
 
@@ -367,7 +364,7 @@
   also have "phi p = nat p - 1"
     by (rule phi_prime, rule assms)
   finally show ?thesis
-    by (metis nat_int) 
+    by (metis nat_int)
 qed
 
 lemma fermat_theorem_nat:
@@ -441,7 +438,7 @@
 lemma wilson_theorem:
   assumes "prime p" shows "[fact (p - 1) = - 1] (mod p)"
 proof (cases "p = 2")
-  case True 
+  case True
   then show ?thesis
     by (simp add: cong_int_def fact_altdef_nat)
 next