		Search-engine friendly clone of the ACL2 documentation.

Edwards-bls12

Edwards-bls12-a

The Edwards-BLS12 coefficient a.

Signature
(edwards-bls12-a) → a
Returns: a — Type (fep a (edwards-bls12-q)).

We show that this coefficient is a square by exhibiting a square root of it.

Definitions and Theorems

Function: edwards-bls12-a

(defun edwards-bls12-a nil
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'edwards-bls12-a))
    (declare (ignorable acl2::__function__))
    (neg 1 (edwards-bls12-q))))

Theorem: return-type-of-edwards-bls12-a

(defthm return-type-of-edwards-bls12-a
  (b* ((a (edwards-bls12-a)))
    (fep a (edwards-bls12-q)))
  :rule-classes :rewrite)

Theorem: edwards-bls12-a-not-zero

(defthm edwards-bls12-a-not-zero
  (not (equal (edwards-bls12-a) 0)))

Theorem: pfield-squarep-of-edwards-bls12-a

(defthm pfield-squarep-of-edwards-bls12-a
  (pfield-squarep (edwards-bls12-a)
                  (edwards-bls12-q)))