		Search-engine friendly clone of the ACL2 documentation.

Elliptic-curves

Pfield-squarep

Check if a prime field element is a square.

This is more general than elliptic curve libraries, but it finds some uses in elliptic curves over prime fields (perhaps this should be moved to the prime field library). We non-constructively check whether there exists a square root in the prime field. The witness function returns a root, if one exists.

Definitions and Theorems

Theorem: pfield-squarep-suff

(defthm pfield-squarep-suff
  (implies (and (fep r p) (equal (mul r r p) x))
           (pfield-squarep x p)))

Theorem: booleanp-of-pfield-squarep

(defthm booleanp-of-pfield-squarep
  (b* ((yes/no (pfield-squarep x p)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Subtopics

Prime-field-squares-euler-criterion: A weak formulation of Euler's criterion for prime field squares.
Pfield-odd-squarep: Check if a prime field element is a square of an odd field element.
Pfield-even-squarep: Check if a prime field element is a square of an even field element.
Pfield-squarep-of-inv: The inverse of x is a prime field square iff x is.