English
In a cancellative commutative monoid with zero that is a Unique Factorization Monoid, if f and g are multisets of irreducible elements and the products f.prod and g.prod are associates, then f and g are associated multisets.
Русский
В моноиде с единичной единицей и нулём, обладающем свойством уникальной факторизации, если f и g — мультидобавки из ирредуцируемых элементов и их произведения ассоциированы, то сами множества факторов ассоциированы.
LaTeX
$$$\text{Let } f,g\in \mathrm{Multiset}(\alpha).\; (\forall x\in f\, \mathrm{Irreducible}(x))\; \&\; (\forall x\in g\, \mathrm{Irreducible}(x))\; (f.prod \sim_u g.prod) \Rightarrow \; \mathrm{Multiset.Rel}(Associated, f, g).$$$
Lean4
theorem factors_unique {f g : Multiset α} (hf : ∀ x ∈ f, Irreducible x) (hg : ∀ x ∈ g, Irreducible x)
(h : f.prod ~ᵤ g.prod) : Multiset.Rel Associated f g :=
prime_factors_unique (fun x hx => UniqueFactorizationMonoid.irreducible_iff_prime.mp (hf x hx))
(fun x hx => UniqueFactorizationMonoid.irreducible_iff_prime.mp (hg x hx)) h
