Unique factorization of natural numbers

Main definitions

• Nat.instUniqueFactorizationMonoid: the natural numbers have unique factorization

instance Nat.instWfDvdMonoid : WfDvdMonoid ℕ

Equations

• Nat.instWfDvdMonoid = ⋯

instance Nat.instUniqueFactorizationMonoid : UniqueFactorizationMonoid ℕ

Equations

• Nat.instUniqueFactorizationMonoid = ⋯

theorem Nat.factors_eq (n : ℕ) : UniqueFactorizationMonoid.normalizedFactors n = ↑n.primeFactorsList

theorem Nat.factors_multiset_prod_of_irreducible {s : Multiset ℕ} (h : ∀ x ∈ s, Irreducible x) : UniqueFactorizationMonoid.normalizedFactors s.prod = s