Theory of univariate polynomials
The theorems include formulas for computing coefficients, such as
coeff_add, coeff_sum, coeff_mul
theorem
polynomial.coeff_sum
{R : Type u}
{S : Type v}
[semiring R]
{p : polynomial R}
[semiring S]
(n : ℕ)
(f : ℕ → R → polynomial S) :
(finsupp.sum p f).coeff n = finsupp.sum p (λ (a : ℕ) (b : R), (f a b).coeff n)
@[simp]
The nth coefficient, as a linear map.
Equations
- polynomial.lcoeff R n = {to_fun := λ (f : polynomial R), f.coeff n, map_add' := _, map_smul' := _}
@[simp]
theorem
polynomial.lcoeff_apply
{R : Type u}
[semiring R]
(n : ℕ)
(f : polynomial R) :
⇑(polynomial.lcoeff R n) f = f.coeff n
@[simp]
theorem
polynomial.coeff_mul_X_zero
{R : Type u}
[semiring R]
(p : polynomial R) :
(p * polynomial.X).coeff 0 = 0
theorem
polynomial.coeff_X_mul_zero
{R : Type u}
[semiring R]
(p : polynomial R) :
(polynomial.X * p).coeff 0 = 0
theorem
polynomial.coeff_C_mul_X
{R : Type u}
[semiring R]
(x : R)
(k n : ℕ) :
(⇑polynomial.C x * polynomial.X ^ k).coeff n = ite (n = k) x 0
@[simp]
theorem
polynomial.C_mul'
{R : Type u}
[semiring R]
(a : R)
(f : polynomial R) :
⇑polynomial.C a * f = a • f
@[simp]
theorem
polynomial.monomial_one_eq_X_pow
{R : Type u}
[semiring R]
{n : ℕ} :
polynomial.monomial n 1 = polynomial.X ^ n
theorem
polynomial.monomial_eq_smul_X
{R : Type u}
{a : R}
[semiring R]
{n : ℕ} :
polynomial.monomial n a = a • polynomial.X ^ n
@[simp]
theorem
polynomial.coeff_X_pow_self
{R : Type u}
[semiring R]
(n : ℕ) :
(polynomial.X ^ n).coeff n = 1
@[simp]
theorem
polynomial.mul_X_pow_eq_zero
{R : Type u}
[semiring R]
{p : polynomial R}
{n : ℕ} :
p * polynomial.X ^ n = 0 → p = 0