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} [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] [SMulZeroClass 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] [SMulZeroClass S R] (r : S) (p : Polynomial R) : (r • p).support ⊆ p.support

theorem Polynomial.card_support_mul_le {R : Type u} [Semiring R] {p q : Polynomial R} : (p * q).support.card ≤ p.support.card * q.support.card

def Polynomial.lsum {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [Semiring A] [AddCommMonoid M] [Module R A] [Module R M] (f : ℕ → A →ₗ[R] M) : Polynomial A →ₗ[R] M

Polynomial.sum as a linear map.

Equations

• Polynomial.lsum f = { toFun := fun (p : Polynomial A) => p.sum fun (x1 : ℕ) (x2 : A) => (f x1) x2, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Polynomial.lsum_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [Semiring R] [Semiring A] [AddCommMonoid M] [Module R A] [Module R M] (f : ℕ → A →ₗ[R] M) (p : Polynomial A) : (lsum f) p = p.sum fun (x1 : ℕ) (x2 : A) => (f x1) x2

def Polynomial.lcoeff (R : Type u) [Semiring R] (n : ℕ) : Polynomial R →ₗ[R] R

The nth coefficient, as a linear map.

Equations

• Polynomial.lcoeff R n = { toFun := fun (p : Polynomial R) => p.coeff n, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Polynomial.lcoeff_apply {R : Type u} [Semiring R] (n : ℕ) (f : Polynomial R) : (lcoeff R n) f = f.coeff n

@[simp]

theorem Polynomial.finsetSum_coeff {R : Type u} [Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial R) (n : ℕ) : (∑ b ∈ s, f b).coeff n = ∑ b ∈ s, (f b).coeff n

theorem Polynomial.coeff_list_sum {R : Type u} [Semiring R] (l : List (Polynomial R)) (n : ℕ) : l.sum.coeff n = (List.map (⇑(lcoeff R n)) l).sum

theorem Polynomial.coeff_list_sum_map {R : Type u} [Semiring R] {ι : Type u_1} (l : List ι) (f : ι → Polynomial R) (n : ℕ) : (List.map f l).sum.coeff n = (List.map (fun (a : ι) => (f a).coeff n) l).sum

@[simp]

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 fun (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 ∈ Finset.antidiagonal n, 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} [Semiring R] (p q : Polynomial R) : (p * q).coeff 0 = p.coeff 0 * q.coeff 0

theorem Polynomial.mul_coeff_one {R : Type u} [Semiring R] (p q : Polynomial R) : (p * q).coeff 1 = p.coeff 0 * q.coeff 1 + p.coeff 1 * q.coeff 0

def Polynomial.constantCoeff {R : Type u} [Semiring R] : Polynomial R →+* R

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 : Polynomial R) => p.coeff 0, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Polynomial.constantCoeff_apply {R : Type u} [Semiring R] (p : Polynomial R) : constantCoeff p = p.coeff 0

theorem Polynomial.constantCoeff_surjective {R : Type u} [Semiring R] : Function.Surjective ⇑constantCoeff

theorem Polynomial.isUnit_C {R : Type u} [Semiring R] {x : R} : IsUnit (C x) ↔ IsUnit x

theorem Polynomial.coeff_mul_X_zero {R : Type u} [Semiring R] (p : Polynomial R) : (p * X).coeff 0 = 0

theorem Polynomial.coeff_X_mul_zero {R : Type u} [Semiring R] (p : Polynomial R) : (X * p).coeff 0 = 0

theorem Polynomial.coeff_C_mul_X_pow {R : Type u} [Semiring R] (x : R) (k n : ℕ) : (C x * X ^ k).coeff n = if n = k then x else 0

theorem Polynomial.coeff_C_mul_X {R : Type u} [Semiring R] (x : R) (n : ℕ) : (C x * X).coeff n = if n = 1 then x else 0

@[simp]

theorem Polynomial.coeff_C_mul {R : Type u} {a : R} {n : ℕ} [Semiring R] (p : Polynomial R) : (C a * p).coeff n = a * p.coeff n

theorem Polynomial.C_mul' {R : Type u} [Semiring R] (a : R) (f : Polynomial R) : C a * f = a • f

@[simp]

theorem Polynomial.coeff_mul_C {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) : (p * C a).coeff n = p.coeff n * a

@[simp]

theorem Polynomial.coeff_mul_natCast {R : Type u} [Semiring R] {p : Polynomial R} {a k : ℕ} : (p * ↑a).coeff k = p.coeff k * ↑a

@[simp]

theorem Polynomial.coeff_natCast_mul {R : Type u} [Semiring R] {p : Polynomial R} {a k : ℕ} : (↑a * p).coeff k = ↑a * p.coeff k

@[simp]

theorem Polynomial.coeff_mul_ofNat {R : Type u} [Semiring R] {p : Polynomial R} {a k : ℕ} [a.AtLeastTwo] : (p * OfNat.ofNat a).coeff k = p.coeff k * OfNat.ofNat a

@[simp]

theorem Polynomial.coeff_ofNat_mul {R : Type u} [Semiring R] {p : Polynomial R} {a k : ℕ} [a.AtLeastTwo] : (OfNat.ofNat a * p).coeff k = OfNat.ofNat a * p.coeff k

@[simp]

theorem Polynomial.coeff_mul_intCast {S : Type v} [Ring S] {p : Polynomial S} {a : ℤ} {k : ℕ} : (p * ↑a).coeff k = p.coeff k * ↑a

@[simp]

theorem Polynomial.coeff_intCast_mul {S : Type v} [Ring S] {p : Polynomial S} {a : ℤ} {k : ℕ} : (↑a * p).coeff k = ↑a * p.coeff k

@[simp]

theorem Polynomial.coeff_X_pow {R : Type u} [Semiring R] (k n : ℕ) : (X ^ k).coeff n = if n = k then 1 else 0

theorem Polynomial.coeff_X_pow_self {R : Type u} [Semiring R] (n : ℕ) : (X ^ 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) : (C x * X ^ k + C y * X ^ m).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) : (C x * X ^ k + C y * X ^ m + C z * X ^ n).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) : (C x * X ^ k + C y * X ^ m).support.card = 2

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) : (C x * X ^ k + C y * X ^ m + C z * X ^ n).support.card = 3

@[simp]

theorem Polynomial.coeff_mul_X_pow {R : Type u} [Semiring R] (p : Polynomial R) (n d : ℕ) : (p * X ^ n).coeff (d + n) = p.coeff d

@[simp]

theorem Polynomial.coeff_X_pow_mul {R : Type u} [Semiring R] (p : Polynomial R) (n d : ℕ) : (X ^ n * p).coeff (d + n) = p.coeff d

theorem Polynomial.coeff_mul_X_pow' {R : Type u} [Semiring R] (p : Polynomial R) (n d : ℕ) : (p * X ^ n).coeff d = if n ≤ d then p.coeff (d - n) else 0

theorem Polynomial.coeff_X_pow_mul' {R : Type u} [Semiring R] (p : Polynomial R) (n d : ℕ) : (X ^ n * p).coeff d = if n ≤ d then p.coeff (d - n) else 0

@[simp]

theorem Polynomial.coeff_mul_X {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : (p * X).coeff (n + 1) = p.coeff n

@[simp]

theorem Polynomial.coeff_X_mul {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : (X * p).coeff (n + 1) = p.coeff n

theorem Polynomial.coeff_mul_monomial {R : Type u} [Semiring R] (p : Polynomial R) (n d : ℕ) (r : R) : (p * (monomial n) 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) : ((monomial n) 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 * (monomial 0) r).coeff d = p.coeff d * r

theorem Polynomial.coeff_monomial_zero_mul {R : Type u} [Semiring R] (p : Polynomial R) (d : ℕ) (r : R) : ((monomial 0) 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 * X ^ n = 0) : p = 0

theorem Polynomial.isRegular_X_pow {R : Type u} [Semiring R] (n : ℕ) : IsRegular (X ^ n)

@[simp]

theorem Polynomial.isRegular_X {R : Type u} [Semiring R] : IsRegular X

theorem Polynomial.X_mem_nonZeroDivisors {R : Type u} [Semiring R] : X ∈ nonZeroDivisors (Polynomial R)

theorem Polynomial.coeff_X_add_C_pow {R : Type u} [Semiring R] (r : R) (n k : ℕ) : ((X + C r) ^ n).coeff k = r ^ (n - k) * ↑(n.choose k)

theorem Polynomial.coeff_X_add_one_pow (R : Type u_1) [Semiring R] (n k : ℕ) : ((X + 1) ^ n).coeff k = ↑(n.choose k)

theorem Polynomial.coeff_one_add_X_pow (R : Type u_1) [Semiring R] (n k : ℕ) : ((1 + X) ^ n).coeff k = ↑(n.choose k)

theorem Polynomial.one_add_X_pow_sub_X_pow {S : Type u_1} [CommRing S] (d : ℕ) : (1 + X) ^ d - X ^ d = ∑ i ∈ Finset.range d, d.choose i • X ^ i

theorem Polynomial.C_dvd_iff_dvd_coeff {R : Type u} [Semiring R] (r : R) (φ : Polynomial R) : C r ∣ φ ↔ ∀ (i : ℕ), r ∣ φ.coeff i

theorem Polynomial.smul_eq_C_mul {R : Type u} [Semiring R] {p : Polynomial R} (a : R) : a • p = C 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 + C (a - p.coeff n) * X ^ n

theorem Polynomial.natCast_coeff_zero {n : ℕ} {R : Type u_1} [Semiring R] : (↑n).coeff 0 = ↑n

theorem Polynomial.natCast_inj {m n : ℕ} {R : Type u_1} [Semiring R] [CharZero R] : ↑m = ↑n ↔ m = n

@[simp]

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

theorem Polynomial.intCast_inj {m n : ℤ} {R : Type u_1} [Ring R] [CharZero R] : ↑m = ↑n ↔ m = n

instance Polynomial.charZero {R : Type u} [Semiring R] [CharZero R] : CharZero (Polynomial R)

instance Polynomial.charP {R : Type u} [Semiring R] {p : ℕ} [CharP R p] : CharP (Polynomial R) p