		Search-engine friendly clone of the ACL2 documentation.

Number-theory

Has-square-root?

Modular square root

Signature
(has-square-root? a p) → y/n
Arguments: a — Guard (natp a).; p — Guard (natp p).
Returns: y/n — Type (booleanp y/n).

Checks if a has a modular square root in the field \mathbb{F}_p, using Euler's criterion.

p must be an odd prime.
0 is considered to have a square root.

Definitions and Theorems

Function: has-square-root?

(defun has-square-root? (a p)
  (declare (xargs :guard (and (natp a) (natp p))))
  (declare (xargs :guard (and (natp a)
                              (primep p)
                              (not (equal p 2))
                              (< a p))))
  (let ((acl2::__function__ 'has-square-root?))
    (declare (ignorable acl2::__function__))
    (and (primep p)
         (or (= a 0)
             (equal (acl2::mod-expt-fast a (/ (- p 1) 2) p)
                    1)))))

Theorem: booleanp-of-has-square-root?

(defthm booleanp-of-has-square-root?
  (b* ((y/n (has-square-root? a p)))
    (booleanp y/n))
  :rule-classes :rewrite)