dvd_irreducible_iff_associated — Mathlib

English

If p and q are irreducible, then p divides q iff p is associated with q.

Русский

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

LaTeX

$$$ [Monoid M] {p q : M} (pp : Irreducible p) (qp : Irreducible q) : p \mid q \iff Associated p q $$$

Lean4

theorem dvd_irreducible_iff_associated [Monoid M] {p q : M} (pp : Irreducible p) (qp : Irreducible q) :
    p ∣ q ↔ Associated p q :=
  ⟨Irreducible.associated_of_dvd pp qp, Associated.dvd⟩

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