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] (n : ℕ) :

polynomial R →ₗ[R] R

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.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) :

(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.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) :

(⇑polynomial.C a) * f = a • f

@[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.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

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 : ℕ) :

(polynomial.X ^ n).coeff n = 1

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 : ℕ} (H : p * polynomial.X ^ n = 0) :

p = 0