Theory of univariate polynomials #
The main results are induction_on and as_sum.
theorem
polynomial.sum_C_mul_X_eq
{R : Type u}
[semiring R]
(p : R[X]) :
p.sum (λ (n : ℕ) (a : R), (⇑polynomial.C a) * polynomial.X ^ n) = p
theorem
polynomial.sum_monomial_eq
{R : Type u}
[semiring R]
(p : R[X]) :
p.sum (λ (n : ℕ) (a : R), ⇑(polynomial.monomial n) a) = p
@[protected]
theorem
polynomial.induction_on
{R : Type u}
[semiring R]
{M : R[X] → Prop}
(p : R[X])
(h_C : ∀ (a : R), M (⇑polynomial.C a))
(h_add : ∀ (p q : R[X]), 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 : R[X] → Prop}
(p : R[X])
(h_add : ∀ (p q : R[X]), 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_coeff_mem_C_inverse
{R : Type u}
[semiring R]
{f : R[X]}
{I : submodule R[X] R[X]}
(cf : ∀ (i : ℕ), f.coeff i ∈ ⇑polynomial.C ⁻¹' I.carrier) :
submodule.span R[X] {g : R[X] | ∃ (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.
theorem
polynomial.mem_span_C_coeff
{R : Type u}
[semiring R]
{f : R[X]} :
f ∈ submodule.span R[X] {g : R[X] | ∃ (i : ℕ), g = ⇑polynomial.C (f.coeff i)}