addX_of_X_eq — Mathlib

English

AddX equals a certain affine expression when the Zs are nonzero; a standard form is provided as addX_eq.

Русский

AddX равен определённому аффинному выражению, когда Z ненуля, формула приведена в addX_eq.

LaTeX

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

Lean4

theorem addX_of_X_eq {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 = addU P Q ^ 2 := by
  rw [addU, neg_sq, div_pow, ← addX_of_X_eq' hP hQ hx, mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz]

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