mathlib3

12b5024b - feat(data/polynomial/erase_lead): add lemma erase_lead_card_support_eq (#5529)

feat(data/polynomial/erase_lead): add lemma erase_lead_card_support_eq (#5529) One further lemma to increase the API of `erase_lead`. I use it to simplify the proof of the Liouville PR. In particular, it is used in a step of the proof that you can "clear denominators" when evaluating a polynomial with integer coefficients at a rational number.