equal
deleted
inserted
replaced
3 Authors: Jeremy Avigad, David Gray, and Adam Kramer |
3 Authors: Jeremy Avigad, David Gray, and Adam Kramer |
4 *) |
4 *) |
5 |
5 |
6 header {* Euler's criterion *} |
6 header {* Euler's criterion *} |
7 |
7 |
8 theory Euler = Residues + EvenOdd:; |
8 theory Euler imports Residues EvenOdd begin; |
9 |
9 |
10 constdefs |
10 constdefs |
11 MultInvPair :: "int => int => int => int set" |
11 MultInvPair :: "int => int => int => int set" |
12 "MultInvPair a p j == {StandardRes p j, StandardRes p (a * (MultInv p j))}" |
12 "MultInvPair a p j == {StandardRes p j, StandardRes p (a * (MultInv p j))}" |
13 SetS :: "int => int => int set set" |
13 SetS :: "int => int => int set set" |