# 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 : ) :
@[simp]
theorem Polynomial.coeff_bit0 {R : Type u} [] (p : ) (n : ) :
@[simp]
theorem Polynomial.coeff_smul {R : Type u} {S : Type v} [] [] (r : S) (p : ) (n : ) :
theorem Polynomial.support_smul {R : Type u} {S : Type v} [] [] (r : S) (p : ) :
theorem Polynomial.card_support_mul_le {R : Type u} [] {p : } {q : } :
(Polynomial.support (p * q)).card .card * .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 = Polynomial.sum p fun (x : ) (x_1 : A) => (f x) x_1
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
• One or more equations did not get rendered due to their size.
Instances For
def Polynomial.lcoeff (R : Type u) [] (n : ) :

The nth coefficient, as a linear map.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Polynomial.lcoeff_apply {R : Type u} [] (n : ) (f : ) :
() f =
@[simp]
theorem Polynomial.finset_sum_coeff {R : Type u} [] {ι : Type u_1} (s : ) (f : ι) (n : ) :
Polynomial.coeff (Finset.sum s fun (b : ι) => f b) n = Finset.sum s fun (b : ι) => Polynomial.coeff (f b) n
theorem Polynomial.coeff_sum {R : Type u} {S : Type v} [] {p : } [] (n : ) (f : R) :
= Polynomial.sum p fun (a : ) (b : R) => Polynomial.coeff (f a b) n
theorem Polynomial.coeff_mul {R : Type u} [] (p : ) (q : ) (n : ) :

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 : ) :
@[simp]
theorem Polynomial.constantCoeff_apply {R : Type u} [] (p : ) :
Polynomial.constantCoeff p =

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

Equations
• One or more equations did not get rendered due to their size.
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 : ) :
Polynomial.coeff (p * Polynomial.X) 0 = 0
theorem Polynomial.coeff_X_mul_zero {R : Type u} [] (p : ) :
Polynomial.coeff (Polynomial.X * p) 0 = 0
theorem Polynomial.coeff_C_mul_X_pow {R : Type u} [] (x : R) (k : ) (n : ) :
Polynomial.coeff (Polynomial.C x * Polynomial.X ^ k) n = if n = k then x else 0
theorem Polynomial.coeff_C_mul_X {R : Type u} [] (x : R) (n : ) :
Polynomial.coeff (Polynomial.C x * Polynomial.X) n = if n = 1 then x else 0
@[simp]
theorem Polynomial.coeff_C_mul {R : Type u} {a : R} {n : } [] (p : ) :
Polynomial.coeff (Polynomial.C a * p) n = a *
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) :
Polynomial.coeff (p * Polynomial.C a) n = * a
@[simp]
theorem Polynomial.coeff_mul_natCast {R : Type u} [] {p : } {a : } {k : } :
Polynomial.coeff (p * a) k = * a
@[simp]
theorem Polynomial.coeff_natCast_mul {R : Type u} [] {p : } {a : } {k : } :
Polynomial.coeff (a * p) k = a *
@[simp]
theorem Polynomial.coeff_mul_ofNat {R : Type u} [] {p : } {a : } {k : } [] :
@[simp]
theorem Polynomial.coeff_ofNat_mul {R : Type u} [] {p : } {a : } {k : } [] :
@[simp]
theorem Polynomial.coeff_mul_intCast {S : Type v} [Ring S] {p : } {a : } {k : } :
Polynomial.coeff (p * a) k = * a
@[simp]
theorem Polynomial.coeff_intCast_mul {S : Type v} [Ring S] {p : } {a : } {k : } :
Polynomial.coeff (a * p) k = a *
@[simp]
theorem Polynomial.coeff_X_pow {R : Type u} [] (k : ) (n : ) :
Polynomial.coeff (Polynomial.X ^ k) n = if n = k then 1 else 0
theorem Polynomial.coeff_X_pow_self {R : Type u} [] (n : ) :
Polynomial.coeff (Polynomial.X ^ n) 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.support (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m) = {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.support (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n) = {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.support (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m)).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.support (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n)).card = 3
@[simp]
theorem Polynomial.coeff_mul_X_pow {R : Type u} [] (p : ) (n : ) (d : ) :
Polynomial.coeff (p * Polynomial.X ^ n) (d + n) =
@[simp]
theorem Polynomial.coeff_X_pow_mul {R : Type u} [] (p : ) (n : ) (d : ) :
Polynomial.coeff (Polynomial.X ^ n * p) (d + n) =
theorem Polynomial.coeff_mul_X_pow' {R : Type u} [] (p : ) (n : ) (d : ) :
Polynomial.coeff (p * Polynomial.X ^ n) d = if n d then Polynomial.coeff p (d - n) else 0
theorem Polynomial.coeff_X_pow_mul' {R : Type u} [] (p : ) (n : ) (d : ) :
Polynomial.coeff (Polynomial.X ^ n * p) d = if n d then Polynomial.coeff p (d - n) else 0
@[simp]
theorem Polynomial.coeff_mul_X {R : Type u} [] (p : ) (n : ) :
Polynomial.coeff (p * Polynomial.X) (n + 1) =
@[simp]
theorem Polynomial.coeff_X_mul {R : Type u} [] (p : ) (n : ) :
Polynomial.coeff (Polynomial.X * p) (n + 1) =
theorem Polynomial.coeff_mul_monomial {R : Type u} [] (p : ) (n : ) (d : ) (r : R) :
Polynomial.coeff (p * r) (d + n) = * r
theorem Polynomial.coeff_monomial_mul {R : Type u} [] (p : ) (n : ) (d : ) (r : R) :
Polynomial.coeff ( r * p) (d + n) = r *
theorem Polynomial.coeff_mul_monomial_zero {R : Type u} [] (p : ) (d : ) (r : R) :
Polynomial.coeff (p * r) d = * r
theorem Polynomial.coeff_monomial_zero_mul {R : Type u} [] (p : ) (d : ) (r : R) :
Polynomial.coeff ( r * p) d = r *
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.coeff ((Polynomial.X + Polynomial.C r) ^ n) k = r ^ (n - k) * ()
theorem Polynomial.coeff_X_add_one_pow (R : Type u_1) [] (n : ) (k : ) :
Polynomial.coeff ((Polynomial.X + 1) ^ n) k = ()
theorem Polynomial.coeff_one_add_X_pow (R : Type u_1) [] (n : ) (k : ) :
Polynomial.coeff ((1 + Polynomial.X) ^ n) k = ()
theorem Polynomial.C_dvd_iff_dvd_coeff {R : Type u} [] (r : R) (φ : ) :
Polynomial.C r φ ∀ (i : ), r
theorem Polynomial.coeff_bit0_mul {R : Type u} [] (P : ) (Q : ) (n : ) :
theorem Polynomial.coeff_bit1_mul {R : Type u} [] (P : ) (Q : ) (n : ) :
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 + Polynomial.C (a - ) * Polynomial.X ^ n
theorem Polynomial.nat_cast_coeff_zero {n : } {R : Type u_1} [] :
Polynomial.coeff (n) 0 = n
theorem Polynomial.nat_cast_inj {m : } {n : } {R : Type u_1} [] [] :
m = n m = n
@[simp]
theorem Polynomial.int_cast_coeff_zero {i : } {R : Type u_1} [Ring R] :
Polynomial.coeff (i) 0 = i
theorem Polynomial.int_cast_inj {m : } {n : } {R : Type u_1} [Ring R] [] :
m = n m = n
instance Polynomial.charZero {R : Type u} [] [] :
Equations
• (_ : ) = (_ : )