# mathlib3documentation

data.polynomial.coeff

# Theory of univariate polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_bit0 {R : Type u} [semiring R] (p : polynomial R) (n : ) :
(bit0 p).coeff n = bit0 (p.coeff n)
@[simp]
theorem polynomial.coeff_smul {R : Type u} {S : Type v} [semiring R] [ 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] [ 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] [ A] [ 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] [ A] [ M] (f : (A →ₗ[R] M)) (p : polynomial A) :
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) :
n) f = f.coeff n
@[simp]
theorem polynomial.finset_sum_coeff {R : Type u} [semiring R] {ι : Type u_1} (s : finset ι) (f : ι ) (n : ) :
(s.sum (λ (b : ι), f b)).coeff n = s.sum (λ (b : ι), (f b).coeff n)
theorem polynomial.coeff_sum {R : Type u} {S : Type v} [semiring R] {p : polynomial R} [semiring S] (n : ) (f : R ) :
(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 : × ), 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
@[simp]
theorem polynomial.constant_coeff_apply {R : Type u} [semiring R] (p : polynomial R) :

constant_coeff p returns the constant term of the polynomial p, defined as coeff p 0. This is a ring homomorphism.

Equations
theorem polynomial.is_unit_C {R : Type u} [semiring R] {x : R} :
theorem polynomial.coeff_mul_X_zero {R : Type u} [semiring R] (p : polynomial R) :
.coeff 0 = 0
theorem polynomial.coeff_X_mul_zero {R : Type u} [semiring R] (p : polynomial R) :
.coeff 0 = 0
theorem polynomial.coeff_C_mul_X_pow {R : Type u} [semiring R] (x : R) (k n : ) :
* .coeff n = ite (n = k) x 0
theorem polynomial.coeff_C_mul_X {R : Type u} [semiring R] (x : R) (n : ) :
n = ite (n = 1) x 0
@[simp]
theorem polynomial.coeff_C_mul {R : Type u} {a : R} {n : } [semiring R] (p : polynomial R) :
* p).coeff n = a * p.coeff n
theorem polynomial.C_mul' {R : Type u} [semiring R] (a : R) (f : polynomial R) :
= a f
@[simp]
theorem polynomial.coeff_mul_C {R : Type u} [semiring R] (p : polynomial R) (n : ) (a : R) :
(p * .coeff n = p.coeff n * a
theorem polynomial.coeff_X_pow {R : Type u} [semiring R] (k n : ) :
.coeff n = ite (n = k) 1 0
@[simp]
theorem polynomial.coeff_X_pow_self {R : Type u} [semiring R] (n : ) :
.coeff n = 1
theorem polynomial.support_binomial {R : Type u} [semiring R] {k m : } (hkm : k m) {x y : R} (hx : x 0) (hy : y 0) :
+ .support = {k, m}
theorem polynomial.support_trinomial {R : Type u} [semiring R] {k m n : } (hkm : k < m) (hmn : m < n) {x y z : R} (hx : x 0) (hy : y 0) (hz : z 0) :
+ + .support = {k, m, n}
theorem polynomial.card_support_binomial {R : Type u} [semiring R] {k m : } (h : k m) {x y : R} (hx : x 0) (hy : y 0) :
theorem polynomial.card_support_trinomial {R : Type u} [semiring R] {k m n : } (hkm : k < m) (hmn : m < n) {x y z : R} (hx : x 0) (hy : y 0) (hz : z 0) :
@[simp]
theorem polynomial.coeff_mul_X_pow {R : Type u} [semiring R] (p : polynomial R) (n d : ) :
(p * .coeff (d + n) = p.coeff d
@[simp]
theorem polynomial.coeff_X_pow_mul {R : Type u} [semiring R] (p : polynomial R) (n d : ) :
* p).coeff (d + n) = p.coeff d
theorem polynomial.coeff_mul_X_pow' {R : Type u} [semiring R] (p : polynomial R) (n d : ) :
(p * .coeff d = ite (n d) (p.coeff (d - n)) 0
theorem polynomial.coeff_X_pow_mul' {R : Type u} [semiring R] (p : polynomial R) (n d : ) :
* p).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 : ) :
.coeff (n + 1) = p.coeff n
@[simp]
theorem polynomial.coeff_X_mul {R : Type u} [semiring R] (p : polynomial R) (n : ) :
.coeff (n + 1) = p.coeff n
theorem polynomial.coeff_mul_monomial {R : Type u} [semiring R] (p : polynomial R) (n d : ) (r : R) :
(p * r).coeff (d + n) = p.coeff d * r
theorem polynomial.coeff_monomial_mul {R : Type u} [semiring R] (p : polynomial R) (n d : ) (r : R) :
( r * p).coeff (d + n) = r * p.coeff d
theorem polynomial.coeff_mul_monomial_zero {R : Type u} [semiring R] (p : polynomial R) (d : ) (r : R) :
(p * r).coeff d = p.coeff d * r
theorem polynomial.coeff_monomial_zero_mul {R : Type u} [semiring R] (p : polynomial R) (d : ) (r : R) :
( r * p).coeff d = r * p.coeff d
theorem polynomial.mul_X_pow_eq_zero {R : Type u} [semiring R] {p : polynomial R} {n : } (H : p * = 0) :
p = 0
theorem polynomial.mul_X_pow_injective {R : Type u} [semiring R] (n : ) :
function.injective (λ (P : , * P)
theorem polynomial.coeff_X_add_C_pow {R : Type u} [semiring R] (r : R) (n k : ) :
^ n).coeff k = r ^ (n - k) * (n.choose k)
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) :
(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) :
a p =
theorem polynomial.update_eq_add_sub_coeff {R : Type u_1} [ring R] (p : polynomial R) (n : ) (a : R) :
p.update n a = p + polynomial.C (a - p.coeff n) *
@[simp]
theorem polynomial.nat_cast_coeff_zero {n : } {R : Type u_1} [semiring R] :
@[simp, norm_cast]
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, norm_cast]
theorem polynomial.int_cast_inj {m n : } {R : Type u_1} [ring R] [char_zero R] :
m = n m = n
@[protected, instance]
def polynomial.char_zero {R : Type u} [semiring R] [char_zero R] :