src/HOL/Old_Number_Theory/Euler.thy
 changeset 61382 efac889fccbc parent 58889 5b7a9633cfa8 child 61649 268d88ec9087
```     1.1 --- a/src/HOL/Old_Number_Theory/Euler.thy	Sat Oct 10 16:21:34 2015 +0200
1.2 +++ b/src/HOL/Old_Number_Theory/Euler.thy	Sat Oct 10 16:26:23 2015 +0200
1.3 @@ -2,7 +2,7 @@
1.5  *)
1.6
1.7 -section {* Euler's criterion *}
1.8 +section \<open>Euler's criterion\<close>
1.9
1.10  theory Euler
1.11  imports Residues EvenOdd
1.12 @@ -15,7 +15,7 @@
1.13    where "SetS a p = MultInvPair a p ` SRStar p"
1.14
1.15
1.16 -subsection {* Property for MultInvPair *}
1.17 +subsection \<open>Property for MultInvPair\<close>
1.18
1.19  lemma MultInvPair_prop1a:
1.20    "[| zprime p; 2 < p; ~([a = 0](mod p));
1.21 @@ -89,7 +89,7 @@
1.22    done
1.23
1.24
1.25 -subsection {* Properties of SetS *}
1.26 +subsection \<open>Properties of SetS\<close>
1.27
1.28  lemma SetS_finite: "2 < p ==> finite (SetS a p)"
1.29    by (auto simp add: SetS_def SRStar_finite [of p])
1.30 @@ -223,14 +223,14 @@
1.31    apply (auto simp add: Union_SetS_setprod_prop2)
1.32    done
1.33
1.34 -text {* \medskip Prove the first part of Euler's Criterion: *}
1.35 +text \<open>\medskip Prove the first part of Euler's Criterion:\<close>
1.36
1.37  lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p));
1.38      ~(QuadRes p x) |] ==>
1.39        [x^(nat (((p) - 1) div 2)) = -1](mod p)"
1.40    by (metis Wilson_Russ zcong_sym zcong_trans zfact_prop)
1.41
1.42 -text {* \medskip Prove another part of Euler Criterion: *}
1.43 +text \<open>\medskip Prove another part of Euler Criterion:\<close>
1.44
1.45  lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)"
1.46  proof -
1.47 @@ -251,7 +251,7 @@
1.48      by (auto simp add: zEven_def zOdd_def)
1.49    then have aux_1: "2 * ((p - 1) div 2) = (p - 1)"
1.50      by (auto simp add: even_div_2_prop2)
1.51 -  with `2 < p` have "1 < (p - 1)"
1.52 +  with \<open>2 < p\<close> have "1 < (p - 1)"
1.53      by auto
1.54    then have " 1 < (2 * ((p - 1) div 2))"
1.55      by (auto simp add: aux_1)
1.56 @@ -268,7 +268,7 @@
1.57    apply (frule zcong_zmult_prop1, auto)
1.58    done
1.59
1.60 -text {* \medskip Prove the final part of Euler's Criterion: *}
1.61 +text \<open>\medskip Prove the final part of Euler's Criterion:\<close>
1.62
1.63  lemma aux__1: "[| ~([x = 0] (mod p)); [y\<^sup>2 = x] (mod p)|] ==> ~(p dvd y)"
1.64    by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div dvd_trans)
1.65 @@ -291,7 +291,7 @@
1.66    done
1.67
1.68
1.69 -text {* \medskip Finally show Euler's Criterion: *}
1.70 +text \<open>\medskip Finally show Euler's Criterion:\<close>
1.71
1.72  theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) =
1.73      a^(nat (((p) - 1) div 2))] (mod p)"
```