		Search-engine friendly clone of the ACL2 documentation.

Pfield-squarep

Pfield-even-squarep

Check if a prime field element is a square of an even field element.

Same as pfield-squarep except restricts the root to be even.

Definitions and Theorems

Theorem: pfield-even-squarep-suff

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

Theorem: booleanp-of-pfield-even-squarep

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