English
Conversely, if R is a UniqueFactorizationMonoid and irreducibles relate by associativity, then there exists HasUnitMulPowIrreducibleFactorization structure for R.
Русский
Напротив, если R является уникальным факторизующим моноидом и ирредуцируемые связаны ассоциированностью, то существует структура HasUnitMulPowIrreducibleFactorization на R.
LaTeX
$$HasUnitMulPowIrreducibleFactorization R$$
Lean4
theorem of_ufd_of_unique_irreducible [UniqueFactorizationMonoid R] (h₁ : ∃ p : R, Irreducible p)
(h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q) : HasUnitMulPowIrreducibleFactorization R :=
by
obtain ⟨p, hp⟩ := h₁
refine ⟨p, hp, ?_⟩
intro x hx
obtain ⟨fx, hfx⟩ := WfDvdMonoid.exists_factors x hx
refine ⟨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
symm
rw [Multiset.eq_replicate]
simp only [true_and, and_imp, Multiset.card_map, Multiset.mem_map, exists_imp]
rintro _ q hq rfl
rw [Associates.mk_eq_mk_iff_associated]
apply h₂ (hfx.1 _ hq) hp
