negY — Mathlib

English

The Y-coordinate of a representative of the negation of a projective point P on a Weierstrass curve is given by negating the Y-coordinate and subtracting the linear terms in X and Z with coefficients a1 and a3.

Русский

Y-координата представителя точки −P на кривой Вейерштрасса равна отрицанию Y-координаты P минус линейные члены по X и Z с коэффициентами a1 и a3.

LaTeX

$$$\\mathrm{negY}(P) = -P_y - W'.a_1\\,P_x - W'.a_3\\,P_z$$$

Lean4

/-- The `Y`-coordinate of a representative of `-P` for a projective point representative `P` on a
Weierstrass curve. -/
def negY (P : Fin 3 → R) : R :=
  -P y - W'.a₁ * P x - W'.a₃ * P z

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