addX_of_Z_ne_zero — Mathlib

English

If the nondegeneracy conditions hold (Z nonzero and appropriate cross-relations), addX equals the affine expression square divided by (Pz Qz)^2.

Русский

При отсутствии вырождения (Z≠0 и прочие условия), AddX равен аффинному выражению, делённому на (Pz Qz)^2.

LaTeX

$$W'.addX P Q = (...) / (P z * Q z) ^ 2$$

Lean4

theorem addX_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) :
    W.addX P Q / addZ P Q ^ 2 =
      W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
        (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)) :=
  by rw [addX_eq hP hQ hPz hQz, toAffine_slope_of_ne hPz hQz hx, toAffine_addX_of_ne hPz hQz <| addZ_ne_zero_of_X_ne hx]

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