English
If every nonzero element has a representation as irreducible factors and factor relations preserve associativity, then unique factorization holds.
Русский
Если каждый ненулевой элемент имеет разложение в ирредуцируемые факторы и сохранение ассоциативности факторов, то факторизация уникальна.
LaTeX
$$$\forall a, a \neq 0 \rightarrow \exists f, (\forall b\in f, \mathrm{Irreducible}(b)) \land f.prod ~ᵤ a \land \forall g, (\forall b\in g, \mathrm{Irreducible}(b)) \rightarrow (\exists! h, \mathrm{Associated}(f.prod, g.prod)).$$$
Lean4
theorem of_existsUnique_irreducible_factors [CancelCommMonoidWithZero α]
(eif : ∀ a : α, a ≠ 0 → ∃ f : Multiset α, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a)
(uif :
∀ f g : Multiset α,
(∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g) :
UniqueFactorizationMonoid α :=
UniqueFactorizationMonoid.of_exists_prime_factors
(by
convert eif using 7
simp_rw [irreducible_iff_prime_of_existsUnique_irreducible_factors eif uif])
