Y_eq_negY_of_Y_eq — Mathlib

English

If hy' and hx hold and P_y equals negY P, then P_y equals negY P.

Русский

Если выполняются гипотезы hy' и hx и P_y = negY P, то P_y = negY P.

LaTeX

$$$ P_y = W'.negY P $$$

Lean4

theorem Y_eq_negY_of_Y_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z)
    (hy : P y * Q z = Q y * P z) (hy' : P y * Q z = W'.negY Q * P z) : P y = W'.negY P :=
  mul_left_injective₀ hQz <| by linear_combination (norm := ring1) -Y_sub_Y_add_Y_sub_negY hx + hy + hy'

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