		Search-engine friendly clone of the ACL2 documentation.

Montgomery

Montgomery-zero

Neutral point of the Montgomery curve group.

Signature
(montgomery-zero) → point
Returns: point — Type (pointp point).

This is the point at infinity.

Definitions and Theorems

Function: montgomery-zero

(defun montgomery-zero nil
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'montgomery-zero))
    (declare (ignorable acl2::__function__))
    (point-infinite)))

Theorem: pointp-of-montgomery-zero

(defthm pointp-of-montgomery-zero
  (b* ((point (montgomery-zero)))
    (pointp point))
  :rule-classes :rewrite)

Theorem: point-on-montgomery-p-of-montgomery-zero

(defthm point-on-montgomery-p-of-montgomery-zero
  (point-on-montgomery-p (montgomery-zero)
                         curve))