equal
deleted
inserted
replaced
1 (* Title: HOL/Old_Number_Theory/Quadratic_Reciprocity.thy |
1 (* Title: HOL/Old_Number_Theory/Quadratic_Reciprocity.thy |
2 Authors: Jeremy Avigad, David Gray, and Adam Kramer |
2 Authors: Jeremy Avigad, David Gray, and Adam Kramer |
3 *) |
3 *) |
4 |
4 |
5 section {* The law of Quadratic reciprocity *} |
5 section \<open>The law of Quadratic reciprocity\<close> |
6 |
6 |
7 theory Quadratic_Reciprocity |
7 theory Quadratic_Reciprocity |
8 imports Gauss |
8 imports Gauss |
9 begin |
9 begin |
10 |
10 |
11 text {* |
11 text \<open> |
12 Lemmas leading up to the proof of theorem 3.3 in Niven and |
12 Lemmas leading up to the proof of theorem 3.3 in Niven and |
13 Zuckerman's presentation. |
13 Zuckerman's presentation. |
14 *} |
14 \<close> |
15 |
15 |
16 context GAUSS |
16 context GAUSS |
17 begin |
17 begin |
18 |
18 |
19 lemma QRLemma1: "a * setsum id A = |
19 lemma QRLemma1: "a * setsum id A = |
151 apply (auto simp add: GAUSS_def) |
151 apply (auto simp add: GAUSS_def) |
152 apply (simp add: GAUSS.A_def [OF GAUSS.intro] GAUSS_def) |
152 apply (simp add: GAUSS.A_def [OF GAUSS.intro] GAUSS_def) |
153 done |
153 done |
154 |
154 |
155 |
155 |
156 subsection {* Stuff about S, S1 and S2 *} |
156 subsection \<open>Stuff about S, S1 and S2\<close> |
157 |
157 |
158 locale QRTEMP = |
158 locale QRTEMP = |
159 fixes p :: "int" |
159 fixes p :: "int" |
160 fixes q :: "int" |
160 fixes q :: "int" |
161 |
161 |