mathlib documentation

data.polynomial.coeff

Theory of univariate polynomials

The theorems include formulas for computing coefficients, such as coeff_add, coeff_sum, coeff_mul

theorem polynomial.coeff_one {R : Type u} [semiring R] (n : ) :
1.coeff n = ite (0 = n) 1 0

@[simp]
theorem polynomial.coeff_add {R : Type u} [semiring R] (p q : polynomial R) (n : ) :
(p + q).coeff n = p.coeff n + q.coeff n

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]
theorem polynomial.coeff_smul {R : Type u} [semiring R] (p : polynomial R) (r : R) (n : ) :
(r p).coeff n = r * p.coeff n

theorem polynomial.mem_support_iff_coeff_ne_zero {R : Type u} {n : } [semiring R] {p : polynomial R} :
n p.support p.coeff n 0

theorem polynomial.not_mem_support_iff_coeff_zero {R : Type u} {n : } [semiring R] {p : polynomial R} :
n p.support p.coeff n = 0

def polynomial.lcoeff (R : Type u) [semiring R] :

The nth coefficient, as a linear map.

Equations
@[simp]
theorem polynomial.lcoeff_apply {R : Type u} [semiring R] (n : ) (f : polynomial R) :

@[simp]
theorem polynomial.finset_sum_coeff {R : Type u} [semiring R] {ι : Type u_1} (s : finset ι) (f : ι → polynomial R) (n : ) :
(∑ (b : ι) in s, f b).coeff n = ∑ (b : ι) in s, (f b).coeff n

theorem polynomial.coeff_mul {R : Type u} [semiring R] (p q : polynomial R) (n : ) :
(p * q).coeff n = ∑ (x : × ) in finset.nat.antidiagonal n, (p.coeff x.fst) * q.coeff x.snd

@[simp]
theorem polynomial.mul_coeff_zero {R : Type u} [semiring R] (p q : polynomial R) :
(p * q).coeff 0 = (p.coeff 0) * q.coeff 0

theorem polynomial.coeff_mul_X_zero {R : Type u} [semiring R] (p : polynomial R) :

theorem polynomial.coeff_X_mul_zero {R : Type u} [semiring R] (p : polynomial R) :

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.coeff_C_mul {R : Type u} {a : R} {n : } [semiring R] (p : polynomial R) :
((polynomial.C a) * p).coeff n = a * p.coeff n

theorem polynomial.C_mul' {R : Type u} [semiring R] (a : R) (f : polynomial R) :

@[simp]
theorem polynomial.coeff_mul_C {R : Type u} [semiring R] (p : polynomial R) (n : ) (a : R) :
(p * polynomial.C a).coeff n = (p.coeff n) * a

theorem polynomial.coeff_X_pow {R : Type u} [semiring R] (k n : ) :
(polynomial.X ^ k).coeff n = ite (n = k) 1 0

@[simp]
theorem polynomial.coeff_X_pow_self {R : Type u} [semiring R] (n : ) :

theorem polynomial.coeff_mul_X_pow {R : Type u} [semiring R] (p : polynomial R) (n d : ) :
(p * polynomial.X ^ n).coeff (d + n) = p.coeff d

@[simp]
theorem polynomial.coeff_mul_X {R : Type u} [semiring R] (p : polynomial R) (n : ) :
(p * polynomial.X).coeff (n + 1) = p.coeff n

theorem polynomial.mul_X_pow_eq_zero {R : Type u} [semiring R] {p : polynomial R} {n : } :
p * polynomial.X ^ n = 0p = 0

theorem polynomial.support_mul_X_pow {R : Type u} [semiring R] (c : R) (n : ) :

theorem polynomial.support_C_mul_X_pow' {R : Type u} [semiring R] {c : R} {n : } :

theorem polynomial.C_dvd_iff_dvd_coeff {R : Type u} [semiring R] (r : R) (φ : polynomial R) :
polynomial.C r φ ∀ (i : ), r φ.coeff i