Y_eq_of_Y_ne — Mathlib

English

A linear combination identity holds: (P_y Q_z - Q_y P_z) + (P_y Q_z - negY Q P_z) equals (P_y - negY P) Q_z.

Русский

Сохраняется линейная комбинация: (P_y Q_z - Q_y P_z) + (P_y Q_z - negY Q P_z) = (P_y - negY P) Q_z.

LaTeX

$$$ (P_y Q_z - Q_y P_z) + (P_y Q_z - W'.negY Q P_z) = (P_y - W'.negY P) Q_z $$$

Lean4

theorem Y_eq_of_Y_ne [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) (hy : P y * Q z ≠ Q y * P z) : P y * Q z = W'.negY Q * P z :=
  sub_eq_zero.mp <|
    (mul_eq_zero.mp <| Y_sub_Y_mul_Y_sub_negY hP hQ hx).resolve_left <|
      mul_ne_zero (mul_ne_zero hPz hQz) <| sub_ne_zero.mpr hy

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