Mathlib v3 is deprecated. Go to Mathlib v4

Def normalization_monoid_of_monoid_hom_right_inverse

Modification history

2020-10-28 18:09

src/algebra/gcd_monoid.lean

feat(ring_theory/unique_factorization_domain): a `normalization_monoid` structure for ufms (#4772) …

Added normalization_monoid_of_monoid_hom_right_inverse View on Github →