isUnit_dblZ_of_Y_ne — Mathlib

English

If hy' holds and the Y-relations hold for P and Q, then dblZ P is nonzero.

Русский

Если выполняются hy' и Y-отношения для P, Q, dblZ P ≠ 0.

LaTeX

$$$W'.Nonsingular P \land W'.Equation P \land W'.Equation Q \land (hy') \Rightarrow W'.dblZ P \neq 0$$$

Lean4

theorem isUnit_dblZ_of_Y_ne {P Q : Fin 3 → F} (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 ≠ Q y * P z ^ 3) : IsUnit (W.dblZ P) :=
  (dblZ_ne_zero_of_Y_ne hP hQ hPz hx hy).isUnit

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