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 : polynomial R) :
finsupp.sum p (λ (n : ℕ) (a : R), (⇑polynomial.C a) * polynomial.X ^ n) = p
theorem
polynomial.sum_monomial_eq
{R : Type u}
[semiring R]
(p : polynomial R) :
finsupp.sum p (λ (n : ℕ) (a : R), ⇑(polynomial.monomial n) a) = p
theorem
polynomial.induction_on
{R : Type u}
[semiring R]
{M : polynomial R → Prop}
(p : polynomial R) :
(∀ (a : R), M (⇑polynomial.C a)) → (∀ (p q : polynomial R), M p → M q → M (p + q)) → (∀ (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) :
(∀ (p q : polynomial R), M p → M q → M (p + q)) → (∀ (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.coeff_mul_monomial
{R : Type u}
[semiring R]
(p : polynomial R)
(n d : ℕ)
(r : R) :
theorem
polynomial.coeff_monomial_mul
{R : Type u}
[semiring R]
(p : polynomial R)
(n d : ℕ)
(r : R) :
theorem
polynomial.coeff_mul_monomial_zero
{R : Type u}
[semiring R]
(p : polynomial R)
(d : ℕ)
(r : R) :
theorem
polynomial.coeff_monomial_zero_mul
{R : Type u}
[semiring R]
(p : polynomial R)
(d : ℕ)
(r : R) :