English
For every nonzero x and irreducible ϖ in a DVR, there exists n ∈ N such that x is associated to ϖ^n.
Русский
Для любого ненулевого x и ирредуцируемого ϖ в DVR существует n ∈ N такое, что x ассоциировано с ϖ^n.
LaTeX
$$$\exists n \in \mathbb{N},\ x \sim ϖ^n$$$
Lean4
theorem associated_pow_irreducible {x : R} (hx : x ≠ 0) {ϖ : R} (hirr : Irreducible ϖ) :
∃ n : ℕ, Associated x (ϖ ^ n) :=
by
have : WfDvdMonoid R := IsNoetherianRing.wfDvdMonoid
obtain ⟨fx, hfx⟩ := WfDvdMonoid.exists_factors x hx
use Multiset.card fx
have H := hfx.2
rw [← Associates.mk_eq_mk_iff_associated] at H ⊢
rw [← H, ← Associates.prod_mk, Associates.mk_pow, ← Multiset.prod_replicate]
congr 1
rw [Multiset.eq_replicate]
simp only [true_and, and_imp, Multiset.card_map, Multiset.mem_map, exists_imp]
rintro _ _ _ rfl
rw [Associates.mk_eq_mk_iff_associated]
refine associated_of_irreducible _ ?_ hirr
apply hfx.1
assumption
