# Documentation

Mathlib.Data.Polynomial.Induction

# Induction on polynomials #

This file contains lemmas dealing with different flavours of induction on polynomials. See also Data/Polynomial/Inductions.lean (with an s!).

The main result is Polynomial.induction_on.

theorem Polynomial.induction_on {R : Type u} [] {M : } (p : ) (h_C : (a : R) → M (Polynomial.C a)) (h_add : (p q : ) → M pM qM (p + q)) (h_monomial : (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} [] {M : } (p : ) (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.span_le_of_C_coeff_mem {R : Type u} [] {f : } {I : Ideal ()} (cf : ∀ (i : ), Polynomial.C () I) :
Ideal.span {g | i, g = Polynomial.C ()} I

If the coefficients of a polynomial belong to an ideal, then that ideal contains the ideal spanned by the coefficients of the polynomial.

theorem Polynomial.mem_span_C_coeff {R : Type u} [] {f : } :
f Ideal.span {g | i, g = Polynomial.C ()}
theorem Polynomial.exists_C_coeff_not_mem {R : Type u} [] {f : } {I : Ideal ()} :
¬f Ii, ¬Polynomial.C () I