dblY — Mathlib

English

The Y-coordinate of the representative of 2P on a Weierstrass Jacobian curve is defined by applying negY to the vector [dblX P, negDblY P, dblZ P].

Русский

Y-координата представителей второй точки 2P на кривой Вейерштрасса задаётся как negY от вектора [dblX P, negDblY P, dblZ P].

LaTeX

$$$\\mathrm{dblY}(P) = \\mathrm{negY}\\Bigl([\\mathrm{dblX}(P), \\mathrm{negDblY}(P), \\mathrm{dblZ}(P)]\\Bigr)$$$

Lean4

/-- The `Y`-coordinate of a representative of `2 • P` for a Jacobian point representative `P` on a
Weierstrass curve. -/
noncomputable def dblY (P : Fin 3 → R) : R :=
  W'.negY ![W'.dblX P, W'.negDblY P, W'.dblZ P]

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