|
|
|---|
|
|
|
|---|
A weak formulation of Euler's criterion for prime field squares.
Euler's criterion serves to determine whether a number is a square or not modulo a prime. See this Wikipedia page.
Here we provide a weaker formulation. It only works for odd prime fields, and it only lets us conclude when a number is not a square.
The criterion is here formulated with respect to the pfield-squarep predicate. Like that predicate, this belongs to a more general library, probably the prime field library itself. It is currently in the elliptic curve library because that is where it is used.
The proof of the criterion relies on some existing libraries. It is explained in this file. It should be possibly to simplify and streamline the proof.
Theorem:
(defthm weak-euler-criterion-contrapositive (implies (and (dm::primep p) (> p 2) (fep a p) (not (equal a 0)) (not (equal (mod (expt a (/ (- p 1) 2)) p) 1))) (not (pfield-squarep a p))))