dblY_of_Z_eq_zero — Mathlib

English

A version of the formula for dblY when P and Q satisfy Weierstrass equations and the Y-relations hold; dblY is expressed in terms of a cubic in P 2.

Русский

Версия формулы для dblY при P и Q, удовлетворяющих уравнениям Weierstrass и Y-отношениям; dblY выражается через кубический член (P 2) и прочие координаты.

LaTeX

$$$ {P Q: Fin 3→F} (hP: W'.Equation P) (hQ: W'.Equation Q) (hPz: P z ≠ 0) (hQz: Q z ≠ 0) (hy': P y Q z = W'.negY Q P z) : W'.dblY P = \text{cubic in coordinates}$$$

Lean4

theorem dblY_of_Z_eq_zero [NoZeroDivisors R] {P : Fin 3 → R} (hP : W'.Equation P) (hPz : P z = 0) :
    W'.dblY P = P y ^ 4 :=
  by
  rw [dblY, negY_eq, negDblY_of_Z_eq_zero hP hPz, dblX_of_Z_eq_zero hP hPz, dblZ_of_Z_eq_zero hPz]
  ring1

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