mathlib3

8fa91251 - feat(data/polynomial/degree/erase_lead): definition and basic lemmas (#4527)

feat(data/polynomial/degree/erase_lead): definition and basic lemmas (#4527) erase_lead serves as the reduction step in an induction, breaking off one monomial from a polynomial. It is used in a later PR to prove that reverse is a multiplicative monoid map on polynomials. Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>