		Search-engine friendly clone of the ACL2 documentation.

Short-weierstrass

Curve-negate

Negate an elliptic curve point.

(curve-negate point p) finds the inverse of point with respect to the elliptic curve group operation.

The result is a point on the elliptic curve.

Note that the curve parameters a and b are irrelevant to this operation, so they are not parameters of this function.

Definitions and Theorems

Function: curve-negate

(defun curve-negate (point p)
  (declare (xargs :guard (and (dm::primep p)
                              (< 3 p)
                              (pointp point)
                              (point-in-pxp-p point p))))
  (if (equal point :infinity)
      point
    (cons (car point) (neg (cdr point) p))))