Induction on polynomials #
This file contains lemmas dealing with different flavours of induction on polynomials.
Data/Polynomial/Inductions.lean (with an
The main result is
To prove something about polynomials, it suffices to show the condition is closed under taking sums, and it holds for monomials.
If the coefficients of a polynomial belong to an ideal, then that ideal contains the ideal spanned by the coefficients of the polynomial.