addZ_of_X_eq — Mathlib

English

If Q_z = 0, then addZ(P,Q) = -(Q_y^2 P_z) P_z.

Русский

Если Q_z = 0, то addZ(P,Q) = -(Q_y^2 P_z) P_z.

LaTeX

$$$Q_z = 0 \Rightarrow W'.addZ(P,Q) = - Q_y^2 P_z^2$$$

Lean4

theorem addZ_of_X_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (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'.addZ P Q = 0 :=
  by
  apply eq_zero_of_ne_zero_of_mul_right_eq_zero <| mul_ne_zero hPz hQz
  rw [addZ_eq' hP hQ, hx, sub_self, zero_pow three_ne_zero]

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