# Unique factorization of natural numbers #

## Main definitions #

- `Nat.instUniqueFactorizationMonoid`: the natural numbers have unique factorization

source
instance Nat.instWfDvdMonoid :
WfDvdMonoid ℕ
source
instance Nat.instUniqueFactorizationMonoid :
UniqueFactorizationMonoid ℕ
source
theorem Nat.factors_eq (n : ℕ) :
UniqueFactorizationMonoid.normalizedFactors n = ↑n.primeFactorsList
source
theorem Nat.factors_multiset_prod_of_irreducible {s : Multiset ℕ} (h : ∀ x ∈ s, Irreducible x) :
UniqueFactorizationMonoid.normalizedFactors s.prod = s