equal
deleted
inserted
replaced
2 |
2 |
3 theory Quadratic_Reciprocity |
3 theory Quadratic_Reciprocity |
4 imports Gauss |
4 imports Gauss |
5 begin |
5 begin |
6 |
6 |
7 text {* The proof is based on Gauss's fifth proof, which can be found at http://www.lehigh.edu/~shw2/q-recip/gauss5.pdf *} |
7 text \<open>The proof is based on Gauss's fifth proof, which can be found at http://www.lehigh.edu/~shw2/q-recip/gauss5.pdf\<close> |
8 |
8 |
9 locale QR = |
9 locale QR = |
10 fixes p :: "nat" |
10 fixes p :: "nat" |
11 fixes q :: "nat" |
11 fixes q :: "nat" |
12 |
12 |