mathlib documentation

data.nat.unique_factorization

source
@[instance]
def nat.wf_dvd_monoid  :
wf_dvd_monoid ℕ

source
@[instance]
def nat.unique_factorization_monoid  :
unique_factorization_monoid ℕ

source
theorem nat.factors_eq {n : ℕ} :
unique_factorization_monoid.factors n = ↑(n.factors)