Commit 2020-09-26 17:53 376ab30f
View on Github →feat(data/nat/unique_factorization): a unique_factorization_monoid instance on N (#4194)
Provides a unique_factorization_monoid instance on nat
Shows its equivalence to nat.factors, which is list-valued