unique_irreducible — Mathlib

English

In a valuation ring, if p and q are irreducible, then they are associated.

Русский

В валюационном кольце два неприводимых элемента p и q автономно связаны ассоциированностью.

LaTeX

$$∀ {p q : R}, \\text{Irreducible } p → \\text{Irreducible } q → \\text{Associated } p q$$

Lean4

theorem unique_irreducible [PreValuationRing R] ⦃p q : R⦄ (hp : Irreducible p) (hq : Irreducible q) : Associated p q :=
  by
  have := dvd_total p q
  rw [Irreducible.dvd_comm hp hq, or_self_iff] at this
  exact associated_of_dvd_dvd (Irreducible.dvd_symm hq hp this) this

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