mathlib

6e5b6cc0 - feat(algebra/gcd_monoid, polynomial/field_division): generalizing `normalization_monoid` on polynomials (#4655)

feat(algebra/gcd_monoid, polynomial/field_division): generalizing `normalization_monoid` on polynomials (#4655) Defines a `normalization_monoid` instance on any `comm_group_with_zero`, including fields Defines a `normalization_monoid` instance on `polynomial R` when `R` has a `normalization_monoid` instance Co-authored-by: Johan Commelin <johan@commelin.net>