mathlib documentation

data.polynomial.induction

Theory of univariate polynomials #

The main results are induction_on and as_sum.

source
theorem polynomial.sum_C_mul_X_eq {R : Type u} [semiring R] (p : polynomial R) :
p.sum (λ (n : ℕ) (a : R), ⇑polynomial.C a * polynomial.X ^ n) = p
source
theorem polynomial.sum_monomial_eq {R : Type u} [semiring R] (p : polynomial R) :
p.sum (λ (n : ℕ) (a : R), ⇑(polynomial.monomial n) a) = p
source
@[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
source
@[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.

source
theorem polynomial.coeff_mul_monomial {R : Type u} [semiring R] (p : polynomial R) (n d : ℕ) (r : R) :
(p * ⇑(polynomial.monomial n) r).coeff (d + n) = p.coeff d * r
source
theorem polynomial.coeff_monomial_mul {R : Type u} [semiring R] (p : polynomial R) (n d : ℕ) (r : R) :
(⇑(polynomial.monomial n) r * p).coeff (d + n) = r * p.coeff d
source
theorem polynomial.coeff_mul_monomial_zero {R : Type u} [semiring R] (p : polynomial R) (d : ℕ) (r : R) :
(p * ⇑(polynomial.monomial 0) r).coeff d = p.coeff d * r
source
theorem polynomial.coeff_monomial_zero_mul {R : Type u} [semiring R] (p : polynomial R) (d : ℕ) (r : R) :
(⇑(polynomial.monomial 0) r * p).coeff d = r * p.coeff d
source
theorem polynomial.span_le_of_coeff_mem_C_inverse {R : Type u} [semiring R] {f : polynomial R} {I : submodule (polynomial R) (polynomial R)} (cf : ∀ (i : ℕ), f.coeff i ∈ ⇑polynomial.C ⁻¹' I.carrier) :
submodule.span (polynomial R) {g : polynomial R | ∃ (i : ℕ), g = ⇑polynomial.C (f.coeff i)} ≤ I

If the coefficients of a polynomial belong to n ideal contains the submodule span of the coefficients of a polynomial.

source
theorem polynomial.mem_span_C_coeff {R : Type u} [semiring R] {f : polynomial R} :
f ∈ submodule.span (polynomial R) {g : polynomial R | ∃ (i : ℕ), g = ⇑polynomial.C (f.coeff i)}
source
theorem polynomial.exists_coeff_not_mem_C_inverse {R : Type u} [semiring R] {f : polynomial R} {I : submodule (polynomial R) (polynomial R)} :
f ∉ I → (∃ (i : ℕ), f.coeff i ∉ ⇑polynomial.C ⁻¹' I.carrier)