negDblY — Mathlib

English

Let P be a point on a Weierstrass curve represented in Jacobian form. The Y-coordinate of a representative of the negation of the double of P, i.e. of −2P, is given by the explicit polynomial expression

Русский

Пусть P — точка на кривой Вейерштрасса в кучной форме. Y-координата представителя точки −2P задаётся явным полиномом

LaTeX

$$$\\operatorname{negDblY}(P) = -W'.\\mathrm{dblU}(P)\\, (W'.\\mathrm{dblX}(P) - P_0\\,(P_1 - W'.\\mathrm{negY}(P))^2) + P_1\\, (P_1 - W'.\\mathrm{negY}(P))^3$$$

Lean4

/-- The `Y`-coordinate of a representative of `-(2 • P)` for a Jacobian point representative `P` on
a Weierstrass curve. -/
noncomputable def negDblY (P : Fin 3 → R) : R :=
  -W'.dblU P * (W'.dblX P - P x * (P y - W'.negY P) ^ 2) + P y * (P y - W'.negY P) ^ 3

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