dblU — Mathlib

English

The unit dblU of a Jacobian point P is equal to the affine expression in coordinates: dblU P = a1 P_y P_z − (3 P_x^2 + 2 a2 P_x P_z^2 + a4 P_z^4).

Русский

Единица dblU точки Якобиана P равна аффинному выражению по координатам: dblU P = a1 P_y P_z − (3 P_x^2 + 2 a2 P_x P_z^2 + a4 P_z^4).

LaTeX

$$$W'.dblU P = W'.a_1 \cdot P_y P_z - \bigl( 3 P_x^2 + 2 W'.a_2 P_x P_z^2 + W'.a_4 P_z^4 \bigr)$$$

Lean4

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

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

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