associated_of_dvd — Mathlib

English

If irreducible p divides irreducible q, then p and q are associated.

Русский

Если иррeдucible p делит irreducible q, то p и q ассоциированы.

LaTeX

$$$ [Monoid M] {p q : M} (p_irr : Irreducible p) (q_irr : Irreducible q) (dvd : p \mid q) : Associated p q $$$

Lean4

theorem associated_of_dvd [Monoid M] {p q : M} (p_irr : Irreducible p) (q_irr : Irreducible q) (dvd : p ∣ q) :
    Associated p q :=
  ((q_irr.dvd_iff.mp dvd).resolve_left p_irr.not_isUnit).symm

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