equal
deleted
inserted
replaced
1 (* Title: HOL/Quadratic_Reciprocity/Quadratic_Reciprocity.thy |
1 (* Title: HOL/Quadratic_Reciprocity/Quadratic_Reciprocity.thy |
|
2 ID: $Id$ |
2 Authors: Jeremy Avigad, David Gray, and Adam Kramer |
3 Authors: Jeremy Avigad, David Gray, and Adam Kramer |
3 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
4 *) |
4 *) |
5 |
5 |
6 header {* The law of Quadratic reciprocity *} |
6 header {* The law of Quadratic reciprocity *} |
7 |
7 |
8 theory Quadratic_Reciprocity = Gauss:; |
8 theory Quadratic_Reciprocity = Gauss:; |