mathlib3

97065dbf - refactor(data/polynomial): use `linear_map` for `monomial`, review `degree` (#4784)