addY — Mathlib

English

The Y-coordinate of the sum P+Q is defined by negY applied to the column vector [addX P Q, negAddY P Q, addZ P Q].

Русский

Y-координата суммы P+Q задаётся как значение negY, применённое к вектору [addX(P,Q), -addY(P,Q), addZ(P,Q)].

LaTeX

$$$$ \\operatorname{addY}(P,Q) = -\\operatorname{Y}([\\operatorname{addX}(P,Q), \\operatorname{negAddY}(P,Q), \\operatorname{addZ}(P,Q)]) $$$$

Lean4

/-- The `Y`-coordinate of a representative of `P + Q` for two distinct Jacobian point
representatives `P` and `Q` on a Weierstrass curve.

If the representatives of `P` and `Q` are equal, then this returns the value `0`. -/
def addY (P Q : Fin 3 → R) : R :=
  W'.negY ![W'.addX P Q, W'.negAddY P Q, addZ P Q]

Похожие утверждения