negDblY_of_Z_ne_zero — Mathlib

English

A variant of negDblY_eq' providing a precise relation between negDblY P and a cubic form of eval P W'.polynomialX with division by P z.

Русский

Вариант negDblY_eq', связывающий negDblY P с кубической формой eval P W'.polynomialX и делением на P z.

LaTeX

$$$ {P} (hP: W'.Equation P) : W'.negDblY P \cdot P z^3 = - eval P W'.polynomialX^3$$$

Lean4

theorem negDblY_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 = Q x * P z) (hy : P y * Q z ≠ W.negY Q * P z) :
    W.negDblY P / W.dblZ P =
      W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
        (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)) :=
  by
  rw [negDblY_eq hP hPz, dblZ, toAffine_slope_of_eq hP hQ hPz hQz hx hy, ← (X_eq_iff hPz hQz).mp hx,
    toAffine_negAddY_of_eq hPz <| sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne' hP hQ hPz hQz hx hy]

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