isUnit_of_irreducible_right — Mathlib

English

If p q with DvdNotUnit, then p is a unit when q is irreducible; otherwise not.

Русский

Если есть связь DvdNotUnit p q, то если q неприводимо, то p является единицей; иначе не обязательно.

LaTeX

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

Lean4

theorem isUnit_of_irreducible_right [CommMonoidWithZero M] {p q : M} (h : DvdNotUnit p q) (hq : Irreducible q) :
    IsUnit p := by
  obtain ⟨_, x, hx, hx'⟩ := h
  exact ((irreducible_iff.1 hq).right hx').resolve_right hx

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