isUnit_addU_of_Y_ne — Mathlib

English

If addU(P,Q) ≠ 0 under the Y-ne condition, then addU(P,Q) is a unit.

Русский

Если addU(P,Q) ≠ 0 по условию Y, тогда addU(P,Q) является единицей.

LaTeX

$$$\\text{IsUnit}(\\mathrm{addU}(P,Q))$ given $\\mathrm{addU}(P,Q) \\neq 0$$$

Lean4

theorem isUnit_addU_of_Y_ne {P Q : Fin 3 → F} (hPz : P z ≠ 0) (hQz : Q z ≠ 0) (hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3) :
    IsUnit (addU P Q) :=
  (addU_ne_zero_of_Y_ne hPz hQz hy).isUnit

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