dblZ_ne_zero_of_Y_ne' — Mathlib

English

NoZeroDivisors ring R; for P,Q with W'.Equation P, W'.Equation Q and P z ≠ 0, Q z ≠ 0, plus cross-relations hx, hy and hy' (different form), we still have W'.dblZ P ≠ 0.

Русский

Без нулевых делителей кольца R; для P,Q с W'.Equation и P z ≠ 0, Q z ≠ 0 и сопутствующими hx, hy и hy', получаем W'.dblZ P ≠ 0.

LaTeX

$$$ [NoZeroDivisors\ R] \; {P,Q} ,\; hP,hQ, hPz, hQz, hx, hy, hy' \Rightarrow W'.dblZ P \neq 0$$$

Lean4

theorem dblZ_ne_zero_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 ≠ W'.negY Q * P z) : W'.dblZ P ≠ 0 :=
  mul_ne_zero hPz <| pow_ne_zero 3 <| sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne' hP hQ hPz hQz hx hy

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