addX_of_X_eq — Mathlib

English

If P_z ≠ 0, Q_z ≠ 0 and P_x Q_z = Q_x P_z, then the X-coordinate of P+Q vanishes: addX(P,Q) = 0.

Русский

Если Pz ≠ 0, Qz ≠ 0 и P_x Q_z = Q_x P_z, то X-координата суммы P+Q равна нулю.

LaTeX

$$$W'.addX(P,Q) = 0\quad\text{если } P_z\neq 0, Q_z\neq 0 \text{ и } P_x Q_z = Q_x P_z.$$$

Lean4

theorem addX_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'.addX P Q = 0 :=
  by
  apply eq_zero_of_ne_zero_of_mul_right_eq_zero <| pow_ne_zero 2 <| mul_ne_zero hPz hQz
  rw [addX_eq' hP hQ, hx]
  ring1

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