src/HOL/Old_Number_Theory/Gauss.thy
 changeset 61382 efac889fccbc parent 58889 5b7a9633cfa8 child 63566 e5abbdee461a
```     1.1 --- a/src/HOL/Old_Number_Theory/Gauss.thy	Sat Oct 10 16:21:34 2015 +0200
1.2 +++ b/src/HOL/Old_Number_Theory/Gauss.thy	Sat Oct 10 16:26:23 2015 +0200
1.3 @@ -2,7 +2,7 @@
1.5  *)
1.6
1.7 -section {* Gauss' Lemma *}
1.8 +section \<open>Gauss' Lemma\<close>
1.9
1.10  theory Gauss
1.11  imports Euler
1.12 @@ -26,7 +26,7 @@
1.13  definition "F = (%x. (p - x)) ` E"
1.14
1.15
1.16 -subsection {* Basic properties of p *}
1.17 +subsection \<open>Basic properties of p\<close>
1.18
1.19  lemma p_odd: "p \<in> zOdd"
1.20    by (auto simp add: p_prime p_g_2 zprime_zOdd_eq_grt_2)
1.21 @@ -64,7 +64,7 @@
1.22    done
1.23
1.24
1.25 -subsection {* Basic Properties of the Gauss Sets *}
1.26 +subsection \<open>Basic Properties of the Gauss Sets\<close>
1.27
1.28  lemma finite_A: "finite (A)"
1.29  by (auto simp add: A_def)
1.30 @@ -272,7 +272,7 @@
1.31  by(rule all_relprime_prod_relprime[OF finite_A all_A_relprime])
1.32
1.33
1.34 -subsection {* Relationships Between Gauss Sets *}
1.35 +subsection \<open>Relationships Between Gauss Sets\<close>
1.36
1.37  lemma B_card_eq_A: "card B = card A"
1.38    using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image)
1.39 @@ -434,7 +434,7 @@
1.40  qed
1.41
1.42
1.43 -subsection {* Gauss' Lemma *}
1.44 +subsection \<open>Gauss' Lemma\<close>
1.45
1.46  lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
1.47    by (auto simp add: finite_E neg_one_special)
```