mathlib3
0831e4f1 - feat(data/polynomial/degree/definitions): add `degree_monoid_hom` (#13233)

Commit
3 years ago
feat(data/polynomial/degree/definitions): add `degree_monoid_hom` (#13233) It will be used to simplify the proof of some lemmas.
Author
Parents
Loading