mathlib3 documentation

data.polynomial.induction

Induction on polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) :

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} :
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)