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)
theorem polynomial.sum_def {R : Type u} {S : Type v} [semiring R] {p : polynomial R} [add_comm_monoid S] (f : R → S) :
finsupp.sum p f = ∑ (n : ) in p.support, f n (p.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
@[simp]
theorem polynomial.mem_support_iff {R : Type u} {n : } [semiring R] {p : polynomial R} :
n p.support p.coeff n 0
theorem polynomial.not_mem_support_iff {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 : ) :

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

Decomposes the coefficient of the product p * q as a sum over nat.antidiagonal. A version which sums over range (n + 1) can be obtained by using finset.nat.sum_antidiagonal_eq_sum_range_succ.

@[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
theorem polynomial.coeff_mul_X_pow' {R : Type u} [semiring R] (p : polynomial R) (n d : ) :
(p * polynomial.X ^ n).coeff d = ite (n d) (p.coeff (d - n)) 0
@[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
theorem polynomial.support_mul_X_pow {R : Type u} [semiring R] (c : R) (n : ) (H : c 0) :
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
theorem polynomial.span_le_of_coeff_mem_C_inverse {R : Type u} [semiring R] {f : polynomial R} {I : submodule (polynomial R) (polynomial R)} (cf : ∀ (i : ), f.coeff i polynomial.C ⁻¹' I.carrier) :
submodule.span (polynomial R) {g : polynomial R | ∃ (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 : polynomial R} :
f submodule.span (polynomial R) {g : polynomial R | ∃ (i : ), g = polynomial.C (f.coeff i)}
theorem polynomial.exists_coeff_not_mem_C_inverse {R : Type u} [semiring R] {f : polynomial R} {I : submodule (polynomial R) (polynomial R)} :
f I(∃ (i : ), f.coeff i polynomial.C ⁻¹' I.carrier)
@[simp]
theorem polynomial.nat_cast_coeff_zero {n : } {R : Type u_1} [semiring R] :
@[simp]
theorem polynomial.nat_cast_inj {m n : } {R : Type u_1} [semiring R] [char_zero R] :
m = n m = n
@[simp]
theorem polynomial.int_cast_coeff_zero {i : } {R : Type u_1} [ring R] :
@[simp]
theorem polynomial.int_cast_inj {m n : } {R : Type u_1} [ring R] [char_zero R] :
m = n m = n