dblY_of_Z_ne_zero — Mathlib

English

A variant formulation stating negDblY P equals (−W'.dblU P)^3 under Y-equality hypotheses.

Русский

Вариант формулировки: при условиях Y-равенства получаем negDblY(P) = (−W'.dblU(P))^3.

LaTeX

$$∀ P, Q with Y-equality conditions, ∶ W'.negDblY P = (−W'.dblU P)^3$$

Lean4

theorem dblY_of_Z_ne_zero [DecidableEq F] {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3) :
    W.dblY P / W.dblZ P ^ 3 =
      W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
        (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)) :=
  by
  erw [dblY, negY_of_Z_ne_zero <| dblZ_ne_zero_of_Y_ne' hP hQ hPz hx hy, dblX_of_Z_ne_zero hP hQ hPz hQz hx hy,
    negDblY_of_Z_ne_zero hP hQ hPz hQz hx hy, Affine.addY]

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