mathlib

490847ee - feat(data/polynomial/degree/lemmas): add induction principle for non-constant polynomials (#8463)

feat(data/polynomial/degree/lemmas): add induction principle for non-constant polynomials (#8463) This PR introduces an induction principle to prove that a property holds for non-constant polynomials. It suffices to check that the property holds for * the sum of a constant polynomial and any polynomial for which the property holds; * the sum of any two polynomials for which the property holds; * for non-constant monomials. I plan to use this to show that polynomials with coefficients in `ℕ` are monotone.