# mathlibdocumentation

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) :
p.sum (λ (n : ) (a : R), * = p
theorem polynomial.sum_monomial_eq {R : Type u} [semiring R] (p : polynomial R) :
p.sum (λ (n : ) (a : R), a) = p
theorem polynomial.induction_on {R : Type u} [semiring R] {M : → Prop} (p : polynomial R) (h_C : ∀ (a : R), M ) (h_add : ∀ (p q : , M pM qM (p + q)) (h_monomial : ∀ (n : ) (a : R), M ((polynomial.C a) * M ((polynomial.C a) * polynomial.X ^ (n + 1))) :
M p
theorem polynomial.induction_on' {R : Type u} [semiring R] {M : → Prop} (p : polynomial R) (h_add : ∀ (p q : , M pM qM (p + q)) (h_monomial : ∀ (n : ) (a : R), M ( 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 * 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) :
(( 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 * r).coeff d = (p.coeff d) * r
theorem polynomial.coeff_monomial_zero_mul {R : Type u} [semiring R] (p : polynomial R) (d : ) (r : R) :
(( r) * p).coeff d = r * p.coeff d
theorem polynomial.span_le_of_coeff_mem_C_inverse {R : Type u} [semiring R] {f : polynomial R} {I : (polynomial R)} (cf : ∀ (i : ), f.coeff i ) :
{g : | ∃ (i : ), g = polynomial.C (f.coeff i)} I

If the coefficients of a polynomial belong to n ideal contains the submodule span of the coefficients of a polynomial.

theorem polynomial.mem_span_C_coeff {R : Type u} [semiring R] {f : polynomial R} :
f {g : | ∃ (i : ), g = polynomial.C (f.coeff i)}
theorem polynomial.exists_coeff_not_mem_C_inverse {R : Type u} [semiring R] {f : polynomial R} {I : (polynomial R)} :
f I(∃ (i : ), f.coeff i