		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)