# 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}
[Semiring R]
{M : Polynomial R → Prop}
(p : Polynomial R)
(h_C : ∀ (a : R), M (Polynomial.C a))
(h_add : ∀ (p q : Polynomial R), M p → M q → M (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}
[Semiring R]
{M : Polynomial R → Prop}
(p : Polynomial R)
(h_add : ∀ (p q : Polynomial R), M p → M q → M (p + q))
(h_monomial : ∀ (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.span_le_of_C_coeff_mem
{R : Type u}
[Semiring R]
{f : Polynomial R}
{I : Ideal (Polynomial R)}
(cf : ∀ (i : ℕ), Polynomial.C (f.coeff i) ∈ I)
:

Ideal.span {g : Polynomial R | ∃ (i : ℕ), g = Polynomial.C (f.coeff i)} ≤ 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}
[Semiring R]
{f : Polynomial R}
:

f ∈ Ideal.span {g : Polynomial R | ∃ (i : ℕ), g = Polynomial.C (f.coeff i)}

theorem
Polynomial.exists_C_coeff_not_mem
{R : Type u}
[Semiring R]
{f : Polynomial R}
{I : Ideal (Polynomial R)}
:

f ∉ I → ∃ (i : ℕ), Polynomial.C (f.coeff i) ∉ I