Commit 2020-10-28 18:09 28cc74f8

View on Github →

feat(ring_theory/unique_factorization_domain): a normalization_monoid structure for ufms (#4772) Provides a default normalization_monoid structure on a unique_factorization_monoid

Estimated changes

Modified src/algebra/associated.lean

added theorem associates.associated_map_mk

added theorem associates.mk_monoid_hom_apply

Modified src/algebra/gcd_monoid.lean

added def normalization_monoid_of_monoid_hom_right_inverse

Modified src/ring_theory/unique_factorization_domain.lean

added theorem unique_factorization_monoid.factors_mul

added theorem unique_factorization_monoid.factors_one