mathlib documentation

data.polynomial.induction

Theory of univariate polynomials

The main results are induction_on and as_sum.

theorem polynomial.sum_C_mul_X_eq {R : Type u} [semiring R] (p : polynomial R) :
finsupp.sum p (λ (n : ) (a : R), (polynomial.C a) * polynomial.X ^ n) = p

theorem polynomial.sum_monomial_eq {R : Type u} [semiring R] (p : polynomial R) :
finsupp.sum p (λ (n : ) (a : R), (polynomial.monomial n) a) = p

theorem polynomial.induction_on {R : Type u} [semiring R] {M : polynomial R → Prop} (p : polynomial R) :
(∀ (a : R), M (polynomial.C a))(∀ (p q : polynomial R), M pM qM (p + q))(∀ (n : ) (a : R), M ((polynomial.C a) * polynomial.X ^ n)M ((polynomial.C a) * polynomial.X ^ (n + 1)))M p

theorem polynomial.induction_on' {R : Type u} [semiring R] {M : polynomial R → Prop} (p : polynomial R) :
(∀ (p q : polynomial R), M pM qM (p + q))(∀ (n : ) (a : R), M ((polynomial.monomial n) a))M p

To prove something about polynomials, it suffices to show the condition is closed under taking sums, and it holds for monomials.

theorem polynomial.coeff_mul_monomial {R : Type u} [semiring R] (p : polynomial R) (n d : ) (r : R) :
(p * (polynomial.monomial n) r).coeff (d + n) = (p.coeff d) * r

theorem polynomial.coeff_monomial_mul {R : Type u} [semiring R] (p : polynomial R) (n d : ) (r : R) :
(((polynomial.monomial n) r) * p).coeff (d + n) = r * p.coeff d

theorem polynomial.coeff_mul_monomial_zero {R : Type u} [semiring R] (p : polynomial R) (d : ) (r : R) :
(p * (polynomial.monomial 0) r).coeff d = (p.coeff d) * r

theorem polynomial.coeff_monomial_zero_mul {R : Type u} [semiring R] (p : polynomial R) (d : ) (r : R) :
(((polynomial.monomial 0) r) * p).coeff d = r * p.coeff d