negDblY_of_Z_eq_zero — Mathlib

English

If P lies on the Weierstrass Jacobian and its Z-coordinate is zero, then negDblY(P) equals −(P_x^2)^3.

Русский

Если точка P на кривой Вейерштрасса имеет Z=0, то negDblY(P) равно −(P_x^2)^3.

LaTeX

$$$W'.\\mathrm{negDblY}(P) = -(P_0^2)^3$$$

Lean4

theorem negDblY_of_Z_eq_zero {P : Fin 3 → R} (hP : W'.Equation P) (hPz : P z = 0) : W'.negDblY P = -(P x ^ 2) ^ 3 := by
  linear_combination (norm :=
    (rw [negDblY, dblU_of_Z_eq_zero hPz, dblX_of_Z_eq_zero hP hPz, negY_of_Z_eq_zero hPz]; ring1))
    (8 * P y ^ 2 - 4 * P x ^ 3) * (equation_of_Z_eq_zero hPz).mp hP

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