mathlib

dc3cbb7d - feat(data/polynomial/erase_lead): introduce two lemmas to compute `nat_degree`s under certain maps (#11265)

feat(data/polynomial/erase_lead): introduce two lemmas to compute `nat_degree`s under certain maps (#11265) This PR is a step in the direction of simplifying #11139. It contains a proof of the helper lemmas `map_nat_degree_eq_sub` and `map_nat_degree_eq_nat_degree` to shorten the proof of `nat_degree_hasse_deriv` and `nat_degree_taylor`. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2311139.20taylor.20sum.20and.20nat_degree_taylor)