mathlib3
6f837a6e - feat(data/polynomial): generalize and rename `polynomial.normalize_monic` (#9853)

Commit
4 years ago
feat(data/polynomial): generalize and rename `polynomial.normalize_monic` (#9853) This PR renames `polynomial.normalize_monic` to `polynomial.monic.normalize_eq_self` (more dot notation!) and generalizes it from fields to `normalization_monoid`s.
Author
Parents
Loading