mathlib
cff99277 - refactor(ring_theory/unique_factorization_domain): rename unique_factorization_monoid.factors (#9503)

Commit

4 years ago

refactor(ring_theory/unique_factorization_domain): rename unique_factorization_monoid.factors (#9503) This frees up the name for the non-normalizing version.

Author

Ruben-VandeVelde

Parents

18e7f914

mathlib cff99277 - refactor(ring_theory/unique_factorization_domain): rename unique_factorization_monoid.factors (#9503)

mathlib
cff99277 - refactor(ring_theory/unique_factorization_domain): rename unique_factorization_monoid.factors (#9503)