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.
@[protected]
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
@[protected]
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)} :