Commit 2022-01-11 20:49 490847ee

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.