addY — Mathlib

English

If P_z ≠ 0 and Q_z ≠ 0, negAddY(P,Q) is a nontrivial homogeneous expression in the coordinates with Weierstrass coefficients.

Русский

При P_z ≠ 0 и Q_z ≠ 0 negAddY(P,Q) является ненулевым однородным выражением координат с коэффициентами кривой.

LaTeX

$$$W'.negAddY(P,Q) = \text{a fixed homogeneous polynomial in }(P_i,Q_i,a_j) \; / \; (P_z Q_z)^2$$$

Lean4

/-- The `Y`-coordinate of a representative of `P + Q` for two distinct projective 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, W'.addZ P Q]

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