not_irreducible_of_not_unit_dvdNotUnit

English

If p is not a unit and DvdNotUnit p q, then q is not irreducible.

Русский

Если p не единица и DvdNotUnit p q, тогда q неразложимо.

LaTeX

$$$\\forall p,q:\\, M,\\; \\lnot \\operatorname{IsUnit}(p) \\land DvdNotUnit(p,q) \\Rightarrow \\lnot \\operatorname{Irreducible}(q).$$$

Lean4

theorem not_irreducible_of_not_unit_dvdNotUnit [CommMonoidWithZero M] {p q : M} (hp : ¬IsUnit p) (h : DvdNotUnit p q) :
    ¬Irreducible q :=
  mt h.isUnit_of_irreducible_right hp

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