dblU — Mathlib

English

The value of the Y-related unit dblU is given by an explicit polynomial in x,y,z: (a1 y z − (3 x^2 + 2 a2 x z + a4 z^2))^3 / z^2.

Русский

Значение dblU выражается явной полиномиальной формулой через координаты x,y,z: (a1 y z − (3 x^2 + 2 a2 x z + a4 z^2))^3 / z^2.

LaTeX

$$$ W.dblU P = \\left( W.a_1 \\; P_y \\; P_z - \\left( 3 P_x^2 + 2 W.a_2 P_x P_z + W.a_4 P_z^2 \\right) \\right)^3 / P_z^2 $$$

Lean4

/-- The unit associated to a representative of `2 • P` for a projective point representative `P` on
a Weierstrass curve `W` that is `2`-torsion.

More specifically, the unit `u` such that `W.add P P = u • ![0, 1, 0]` where `P = W.neg P`. -/
noncomputable def dblU (P : Fin 3 → F) : F :=
  eval P W.polynomialX ^ 3 / P z ^ 2

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