negAddY_of_Z_ne_zero — Mathlib

English

If P_z = 0, then negAddY(P,Q) equals a certain simple expression in P_y, P_z, Q coordinates with the a_i coefficients.

Русский

Если P_z = 0, то negAddY(P,Q) упрощается до выражения через P_y, координаты Q и коэффициенты a_i.

LaTeX

$$$W'.negAddY(P,Q) = (P_y,\ldots) \; \text{(simplified form when }P_z=0$).$$

Lean4

theorem negAddY_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) :
    W.negAddY P Q / W.addZ P Q =
      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 [negAddY_eq hP hQ hPz hQz, addZ_eq hP hQ hPz hQz, toAffine_slope_of_ne hPz hQz hx,
    toAffine_negAddY_of_ne hPz hQz <| sub_ne_zero.mpr hx]

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