isUnit_iff_not_associated_of_dvd — Mathlib

English

In a monoid, if x is irreducible and y divides x, then y is a unit if and only if x and y are not associated.

Русский

В моноиде, если x неприводим и y делит x, тогда y — единица тогда и только тогда, когда x и y не ассоциированы.

LaTeX

$$$$\forall M \,[\mathrm{Monoid}\, M], \mathrm{Irreducible}(x) \land (y \mid x) \Rightarrow (\mathrm{IsUnit}(y) \iff \neg \mathrm{Associated}(x,y)).$$$$

Lean4

theorem isUnit_iff_not_associated_of_dvd [Monoid M] {x y : M} (hx : Irreducible x) (hy : y ∣ x) :
    IsUnit y ↔ ¬Associated x y :=
  ⟨fun hy hxy => hx.1 (hxy.symm.isUnit hy), (hx.dvd_iff.mp hy).resolve_right⟩

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