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