# Theory of univariate polynomials #

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

@[simp]
theorem Polynomial.coeff_add {R : Type u} [] (p : ) (q : ) (n : ) :
(p + q).coeff n = p.coeff n + q.coeff n
@[simp]
theorem Polynomial.coeff_smul {R : Type u} {S : Type v} [] [] (r : S) (p : ) (n : ) :
(r p).coeff n = r p.coeff n
theorem Polynomial.support_smul {R : Type u} {S : Type v} [] [] (r : S) (p : ) :
(r p).support p.support
theorem Polynomial.card_support_mul_le {R : Type u} [] {p : } {q : } :
(p * q).support.card p.support.card * q.support.card
@[simp]
theorem Polynomial.lsum_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [] [] [] [Module R A] [Module R M] (f : A →ₗ[R] M) (p : ) :
p = p.sum fun (x1 : ) (x2 : A) => (f x1) x2
def Polynomial.lsum {R : Type u_1} {A : Type u_2} {M : Type u_3} [] [] [] [Module R A] [Module R M] (f : A →ₗ[R] M) :

Polynomial.sum as a linear map.

Equations
• = { toFun := fun (p : ) => p.sum fun (x1 : ) (x2 : A) => (f x1) x2, map_add' := , map_smul' := }
Instances For
def Polynomial.lcoeff (R : Type u) [] (n : ) :

The nth coefficient, as a linear map.

Equations
• = { toFun := fun (p : ) => p.coeff n, map_add' := , map_smul' := }
Instances For
@[simp]
theorem Polynomial.lcoeff_apply {R : Type u} [] (n : ) (f : ) :
f = f.coeff n
@[simp]
theorem Polynomial.finset_sum_coeff {R : Type u} [] {ι : Type u_1} (s : ) (f : ι) (n : ) :
(∑ bs, f b).coeff n = bs, (f b).coeff n
theorem Polynomial.coeff_list_sum {R : Type u} [] (l : List (Polynomial R)) (n : ) :
l.sum.coeff n = (List.map (⇑) l).sum
theorem Polynomial.coeff_list_sum_map {R : Type u} [] {ι : Type u_1} (l : List ι) (f : ι) (n : ) :
(List.map f l).sum.coeff n = (List.map (fun (a : ι) => (f a).coeff n) l).sum
theorem Polynomial.coeff_sum {R : Type u} {S : Type v} [] {p : } [] (n : ) (f : R) :
(p.sum f).coeff n = p.sum fun (a : ) (b : R) => (f a b).coeff n
theorem Polynomial.coeff_mul {R : Type u} [] (p : ) (q : ) (n : ) :
(p * q).coeff n = x, p.coeff x.1 * q.coeff x.2

Decomposes the coefficient of the product p * q as a sum over 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} [] (p : ) (q : ) :
(p * q).coeff 0 = p.coeff 0 * q.coeff 0
theorem Polynomial.mul_coeff_one {R : Type u} [] (p : ) (q : ) :
(p * q).coeff 1 = p.coeff 0 * q.coeff 1 + p.coeff 1 * q.coeff 0
@[simp]
theorem Polynomial.constantCoeff_apply {R : Type u} [] (p : ) :
Polynomial.constantCoeff p = p.coeff 0

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

Equations
• Polynomial.constantCoeff = { toFun := fun (p : ) => p.coeff 0, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
theorem Polynomial.isUnit_C {R : Type u} [] {x : R} :
IsUnit (Polynomial.C x)
theorem Polynomial.coeff_mul_X_zero {R : Type u} [] (p : ) :
(p * Polynomial.X).coeff 0 = 0
theorem Polynomial.coeff_X_mul_zero {R : Type u} [] (p : ) :
(Polynomial.X * p).coeff 0 = 0
theorem Polynomial.coeff_C_mul_X_pow {R : Type u} [] (x : R) (k : ) (n : ) :
(Polynomial.C x * Polynomial.X ^ k).coeff n = if n = k then x else 0
theorem Polynomial.coeff_C_mul_X {R : Type u} [] (x : R) (n : ) :
(Polynomial.C x * Polynomial.X).coeff n = if n = 1 then x else 0
@[simp]
theorem Polynomial.coeff_C_mul {R : Type u} {a : R} {n : } [] (p : ) :
(Polynomial.C a * p).coeff n = a * p.coeff n
theorem Polynomial.C_mul' {R : Type u} [] (a : R) (f : ) :
Polynomial.C a * f = a f
@[simp]
theorem Polynomial.coeff_mul_C {R : Type u} [] (p : ) (n : ) (a : R) :
(p * Polynomial.C a).coeff n = p.coeff n * a
@[simp]
theorem Polynomial.coeff_mul_natCast {R : Type u} [] {p : } {a : } {k : } :
(p * a).coeff k = p.coeff k * a
@[simp]
theorem Polynomial.coeff_natCast_mul {R : Type u} [] {p : } {a : } {k : } :
(a * p).coeff k = a * p.coeff k
@[simp]
theorem Polynomial.coeff_mul_ofNat {R : Type u} [] {p : } {a : } {k : } [a.AtLeastTwo] :
(p * ).coeff k = p.coeff k *
@[simp]
theorem Polynomial.coeff_ofNat_mul {R : Type u} [] {p : } {a : } {k : } [a.AtLeastTwo] :
( * p).coeff k = * p.coeff k
@[simp]
theorem Polynomial.coeff_mul_intCast {S : Type v} [Ring S] {p : } {a : } {k : } :
(p * a).coeff k = p.coeff k * a
@[simp]
theorem Polynomial.coeff_intCast_mul {S : Type v} [Ring S] {p : } {a : } {k : } :
(a * p).coeff k = a * p.coeff k
@[simp]
theorem Polynomial.coeff_X_pow {R : Type u} [] (k : ) (n : ) :
(Polynomial.X ^ k).coeff n = if n = k then 1 else 0
theorem Polynomial.coeff_X_pow_self {R : Type u} [] (n : ) :
(Polynomial.X ^ n).coeff n = 1
theorem Polynomial.support_binomial {R : Type u} [] {k : } {m : } (hkm : k m) {x : R} {y : R} (hx : x 0) (hy : y 0) :
(Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support = {k, m}
theorem Polynomial.support_trinomial {R : Type u} [] {k : } {m : } {n : } (hkm : k < m) (hmn : m < n) {x : R} {y : R} {z : R} (hx : x 0) (hy : y 0) (hz : z 0) :
(Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n).support = {k, m, n}
theorem Polynomial.card_support_binomial {R : Type u} [] {k : } {m : } (h : k m) {x : R} {y : R} (hx : x 0) (hy : y 0) :
(Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support.card = 2
theorem Polynomial.card_support_trinomial {R : Type u} [] {k : } {m : } {n : } (hkm : k < m) (hmn : m < n) {x : R} {y : R} {z : R} (hx : x 0) (hy : y 0) (hz : z 0) :
(Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n).support.card = 3
@[simp]
theorem Polynomial.coeff_mul_X_pow {R : Type u} [] (p : ) (n : ) (d : ) :
(p * Polynomial.X ^ n).coeff (d + n) = p.coeff d
@[simp]
theorem Polynomial.coeff_X_pow_mul {R : Type u} [] (p : ) (n : ) (d : ) :
(Polynomial.X ^ n * p).coeff (d + n) = p.coeff d
theorem Polynomial.coeff_mul_X_pow' {R : Type u} [] (p : ) (n : ) (d : ) :
(p * Polynomial.X ^ n).coeff d = if n d then p.coeff (d - n) else 0
theorem Polynomial.coeff_X_pow_mul' {R : Type u} [] (p : ) (n : ) (d : ) :
(Polynomial.X ^ n * p).coeff d = if n d then p.coeff (d - n) else 0
@[simp]
theorem Polynomial.coeff_mul_X {R : Type u} [] (p : ) (n : ) :
(p * Polynomial.X).coeff (n + 1) = p.coeff n
@[simp]
theorem Polynomial.coeff_X_mul {R : Type u} [] (p : ) (n : ) :
(Polynomial.X * p).coeff (n + 1) = p.coeff n
theorem Polynomial.coeff_mul_monomial {R : Type u} [] (p : ) (n : ) (d : ) (r : R) :
(p * r).coeff (d + n) = p.coeff d * r
theorem Polynomial.coeff_monomial_mul {R : Type u} [] (p : ) (n : ) (d : ) (r : R) :
( r * p).coeff (d + n) = r * p.coeff d
theorem Polynomial.coeff_mul_monomial_zero {R : Type u} [] (p : ) (d : ) (r : R) :
(p * r).coeff d = p.coeff d * r
theorem Polynomial.coeff_monomial_zero_mul {R : Type u} [] (p : ) (d : ) (r : R) :
( r * p).coeff d = r * p.coeff d
theorem Polynomial.mul_X_pow_eq_zero {R : Type u} [] {p : } {n : } (H : p * Polynomial.X ^ n = 0) :
p = 0
theorem Polynomial.isRegular_X_pow {R : Type u} [] (n : ) :
IsRegular (Polynomial.X ^ n)
@[simp]
theorem Polynomial.isRegular_X {R : Type u} [] :
IsRegular Polynomial.X
theorem Polynomial.coeff_X_add_C_pow {R : Type u} [] (r : R) (n : ) (k : ) :
((Polynomial.X + Polynomial.C r) ^ n).coeff k = r ^ (n - k) * (n.choose k)
theorem Polynomial.coeff_X_add_one_pow (R : Type u_1) [] (n : ) (k : ) :
((Polynomial.X + 1) ^ n).coeff k = (n.choose k)
theorem Polynomial.coeff_one_add_X_pow (R : Type u_1) [] (n : ) (k : ) :
((1 + Polynomial.X) ^ n).coeff k = (n.choose k)
theorem Polynomial.C_dvd_iff_dvd_coeff {R : Type u} [] (r : R) (φ : ) :
Polynomial.C r φ ∀ (i : ), r φ.coeff i
theorem Polynomial.smul_eq_C_mul {R : Type u} [] {p : } (a : R) :
a p = Polynomial.C a * p
theorem Polynomial.update_eq_add_sub_coeff {R : Type u_1} [Ring R] (p : ) (n : ) (a : R) :
p.update n a = p + Polynomial.C (a - p.coeff n) * Polynomial.X ^ n
theorem Polynomial.natCast_coeff_zero {n : } {R : Type u_1} [] :
(↑n).coeff 0 = n
@[deprecated Polynomial.natCast_coeff_zero]
theorem Polynomial.nat_cast_coeff_zero {n : } {R : Type u_1} [] :
(↑n).coeff 0 = n

Alias of Polynomial.natCast_coeff_zero.

theorem Polynomial.natCast_inj {m : } {n : } {R : Type u_1} [] [] :
m = n m = n
@[deprecated Polynomial.natCast_inj]
theorem Polynomial.nat_cast_inj {m : } {n : } {R : Type u_1} [] [] :
m = n m = n

Alias of Polynomial.natCast_inj.

@[simp]
theorem Polynomial.intCast_coeff_zero {i : } {R : Type u_1} [Ring R] :
(↑i).coeff 0 = i
@[deprecated Polynomial.intCast_coeff_zero]
theorem Polynomial.int_cast_coeff_zero {i : } {R : Type u_1} [Ring R] :
(↑i).coeff 0 = i

Alias of Polynomial.intCast_coeff_zero.

theorem Polynomial.intCast_inj {m : } {n : } {R : Type u_1} [Ring R] [] :
m = n m = n
@[deprecated Polynomial.intCast_inj]
theorem Polynomial.int_cast_inj {m : } {n : } {R : Type u_1} [Ring R] [] :
m = n m = n

Alias of Polynomial.intCast_inj.

instance Polynomial.charZero {R : Type u} [] [] :
Equations
• =