mathlib

c2fcf9f1 - feat(data/polynomial/erase_lead): Characterizations of polynomials of small support (#14500)

feat(data/polynomial/erase_lead): Characterizations of polynomials of small support (#14500) This PR adds iff-lemmas `card_support_eq_one`, `card_support_eq_two`, and `card_support_eq_three`. These will be useful for irreducibility of x^n-x-1.