negY — Mathlib

English

Definition of the Y-coordinate representative of a negative point on a Weierstrass Jacobian.

Русский

Определение координаты Y для представителя отрицательной точки на Якобиане Вейерштрасса.

LaTeX

$$$$ \\text{def negY}(P) = -P_y - W'.a_1 \\cdot P_x \\cdot P_z - W'.a_3 \\cdot P_z^3 $$$$

Lean4

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

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