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
@[simp]
theorem polynomial.coeff_smul {R : Type u} {S : Type v} [semiring R] [monoid S] [distrib_mul_action S R] (r : S) (p : polynomial R) (n : ) :
(r p).coeff n = r p.coeff n
theorem polynomial.support_smul {R : Type u} {S : Type v} [semiring R] [monoid S] [distrib_mul_action S R] (r : S) (p : polynomial R) :
def polynomial.lsum {R : Type u_1} {A : Type u_2} {M : Type u_3} [semiring R] [semiring A] [add_comm_monoid M] [module R A] [module R M] (f : (A →ₗ[R] M)) :

polynomial.sum as a linear map.

Equations
@[simp]
theorem polynomial.lsum_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [semiring R] [semiring A] [add_comm_monoid M] [module R A] [module R M] (f : (A →ₗ[R] M)) (p : polynomial A) :
(polynomial.lsum f) p = p.sum (λ (n : ) (r : A), (f n) r)
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_sum {R : Type u} {S : Type v} [semiring R] {p : polynomial R} [semiring S] (n : ) (f : R → polynomial S) :
(p.sum f).coeff n = p.sum (λ (a : ) (b : R), (f a 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.coeff_X_add_one_pow (R : Type u_1) [semiring R] (n k : ) :
((polynomial.X + 1) ^ n).coeff k = (n.choose k)
theorem polynomial.coeff_one_add_X_pow (R : Type u_1) [semiring R] (n k : ) :
((1 + polynomial.X) ^ n).coeff k = (n.choose k)
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.coeff_bit0_mul {R : Type u} [semiring R] (P Q : polynomial R) (n : ) :
((bit0 P) * Q).coeff n = 2 * (P * Q).coeff n
theorem polynomial.coeff_bit1_mul {R : Type u} [semiring R] (P Q : polynomial R) (n : ) :
((bit1 P) * Q).coeff n = 2 * (P * Q).coeff n + Q.coeff n
theorem polynomial.smul_eq_C_mul {R : Type u} [semiring R] {p : polynomial R} (a : R) :
theorem polynomial.update_eq_add_sub_coeff {R : Type u_1} [ring R] (p : polynomial R) (n : ) (a : R) :
@[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