dblZ_ne_zero_of_Y_ne' — Mathlib

English

Under W.Equation constraints and hy, dblZ P is nonzero given Y-relations with Q.

Русский

При условиях W.Equation и hy, dblZ P ≠ 0.

LaTeX

$$$W'.Equation P \land W'.Equation Q \land hx \land 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) (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 ≠ W'.negY Q * P z ^ 3) : W'.dblZ P ≠ 0 :=
  mul_ne_zero hPz <| sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne' hP hQ hx hy

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