Documentation

Mathlib.Data.Polynomial.Coeff

Theory of univariate polynomials #

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

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

    The nth coefficient, as a linear map.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem Polynomial.lcoeff_apply {R : Type u} [Semiring R] (n : ℕ) (f : Polynomial R) :
      (Polynomial.lcoeff R n) f = Polynomial.coeff f n
      source
      @[simp]
      theorem Polynomial.finset_sum_coeff {R : Type u} [Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial R) (n : ℕ) :
      Polynomial.coeff (Finset.sum s fun (b : ι) => f b) n = Finset.sum s fun (b : ι) => Polynomial.coeff (f b) n
      source
      theorem Polynomial.coeff_sum {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (n : ℕ) (f : ℕ → R → Polynomial S) :
      Polynomial.coeff (Polynomial.sum p f) n = Polynomial.sum p fun (a : ℕ) (b : R) => Polynomial.coeff (f a b) n
      source
      theorem Polynomial.coeff_mul {R : Type u} [Semiring R] (p : Polynomial R) (q : Polynomial R) (n : ℕ) :
      Polynomial.coeff (p * q) n = Finset.sum (Finset.antidiagonal n) fun (x : ℕ × ℕ) => Polynomial.coeff p x.1 * Polynomial.coeff q 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.

      source
      @[simp]
      theorem Polynomial.mul_coeff_zero {R : Type u} [Semiring R] (p : Polynomial R) (q : Polynomial R) :
      Polynomial.coeff (p * q) 0 = Polynomial.coeff p 0 * Polynomial.coeff q 0
      source
      @[simp]
      theorem Polynomial.constantCoeff_apply {R : Type u} [Semiring R] (p : Polynomial R) :
      Polynomial.constantCoeff p = Polynomial.coeff p 0
      source
      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
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Polynomial.isUnit_C {R : Type u} [Semiring R] {x : R} :
        IsUnit (Polynomial.C x) ↔ IsUnit x
        source
        theorem Polynomial.coeff_mul_X_zero {R : Type u} [Semiring R] (p : Polynomial R) :
        Polynomial.coeff (p * Polynomial.X) 0 = 0
        source
        theorem Polynomial.coeff_X_mul_zero {R : Type u} [Semiring R] (p : Polynomial R) :
        Polynomial.coeff (Polynomial.X * p) 0 = 0
        source
        theorem Polynomial.coeff_C_mul_X_pow {R : Type u} [Semiring R] (x : R) (k : ℕ) (n : ℕ) :
        Polynomial.coeff (Polynomial.C x * Polynomial.X ^ k) n = if n = k then x else 0
        source
        theorem Polynomial.coeff_C_mul_X {R : Type u} [Semiring R] (x : R) (n : ℕ) :
        Polynomial.coeff (Polynomial.C x * Polynomial.X) n = if n = 1 then x else 0
        source
        @[simp]
        theorem Polynomial.coeff_C_mul {R : Type u} {a : R} {n : ℕ} [Semiring R] (p : Polynomial R) :
        Polynomial.coeff (Polynomial.C a * p) n = a * Polynomial.coeff p n
        source
        theorem Polynomial.C_mul' {R : Type u} [Semiring R] (a : R) (f : Polynomial R) :
        Polynomial.C a * f = a • f
        source
        @[simp]
        theorem Polynomial.coeff_mul_C {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) :
        Polynomial.coeff (p * Polynomial.C a) n = Polynomial.coeff p n * a
        source
        @[simp]
        theorem Polynomial.coeff_mul_natCast {R : Type u} [Semiring R] {p : Polynomial R} {a : ℕ} {k : ℕ} :
        Polynomial.coeff (p * ↑a) k = Polynomial.coeff p k * ↑a
        source
        @[simp]
        theorem Polynomial.coeff_natCast_mul {R : Type u} [Semiring R] {p : Polynomial R} {a : ℕ} {k : ℕ} :
        Polynomial.coeff (↑a * p) k = ↑a * Polynomial.coeff p k
        source
        @[simp]
        theorem Polynomial.coeff_mul_ofNat {R : Type u} [Semiring R] {p : Polynomial R} {a : ℕ} {k : ℕ} [Nat.AtLeastTwo a] :
        Polynomial.coeff (p * OfNat.ofNat a) k = Polynomial.coeff p k * OfNat.ofNat a
        source
        @[simp]
        theorem Polynomial.coeff_ofNat_mul {R : Type u} [Semiring R] {p : Polynomial R} {a : ℕ} {k : ℕ} [Nat.AtLeastTwo a] :
        Polynomial.coeff (OfNat.ofNat a * p) k = OfNat.ofNat a * Polynomial.coeff p k
        source
        @[simp]
        theorem Polynomial.coeff_mul_intCast {S : Type v} [Ring S] {p : Polynomial S} {a : ℤ} {k : ℕ} :
        Polynomial.coeff (p * ↑a) k = Polynomial.coeff p k * ↑a
        source
        @[simp]
        theorem Polynomial.coeff_intCast_mul {S : Type v} [Ring S] {p : Polynomial S} {a : ℤ} {k : ℕ} :
        Polynomial.coeff (↑a * p) k = ↑a * Polynomial.coeff p k
        source
        @[simp]
        theorem Polynomial.coeff_X_pow {R : Type u} [Semiring R] (k : ℕ) (n : ℕ) :
        Polynomial.coeff (Polynomial.X ^ k) n = if n = k then 1 else 0
        source
        theorem Polynomial.coeff_X_pow_self {R : Type u} [Semiring R] (n : ℕ) :
        Polynomial.coeff (Polynomial.X ^ n) n = 1
        source
        theorem Polynomial.support_binomial {R : Type u} [Semiring R] {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}
        source
        theorem Polynomial.support_trinomial {R : Type u} [Semiring R] {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}
        source
        theorem Polynomial.card_support_binomial {R : Type u} [Semiring R] {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
        source
        theorem Polynomial.card_support_trinomial {R : Type u} [Semiring R] {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
        source
        @[simp]
        theorem Polynomial.coeff_mul_X_pow {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (d : ℕ) :
        Polynomial.coeff (p * Polynomial.X ^ n) (d + n) = Polynomial.coeff p d
        source
        @[simp]
        theorem Polynomial.coeff_X_pow_mul {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (d : ℕ) :
        Polynomial.coeff (Polynomial.X ^ n * p) (d + n) = Polynomial.coeff p d
        source
        theorem Polynomial.coeff_mul_X_pow' {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (d : ℕ) :
        Polynomial.coeff (p * Polynomial.X ^ n) d = if n ≤ d then Polynomial.coeff p (d - n) else 0
        source
        theorem Polynomial.coeff_X_pow_mul' {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (d : ℕ) :
        Polynomial.coeff (Polynomial.X ^ n * p) d = if n ≤ d then Polynomial.coeff p (d - n) else 0
        source
        @[simp]
        theorem Polynomial.coeff_mul_X {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) :
        Polynomial.coeff (p * Polynomial.X) (n + 1) = Polynomial.coeff p n
        source
        @[simp]
        theorem Polynomial.coeff_X_mul {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) :
        Polynomial.coeff (Polynomial.X * p) (n + 1) = Polynomial.coeff p n
        source
        theorem Polynomial.coeff_mul_monomial {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (d : ℕ) (r : R) :
        Polynomial.coeff (p * (Polynomial.monomial n) r) (d + n) = Polynomial.coeff p d * r
        source
        theorem Polynomial.coeff_monomial_mul {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (d : ℕ) (r : R) :
        Polynomial.coeff ((Polynomial.monomial n) r * p) (d + n) = r * Polynomial.coeff p d
        source
        theorem Polynomial.coeff_mul_monomial_zero {R : Type u} [Semiring R] (p : Polynomial R) (d : ℕ) (r : R) :
        Polynomial.coeff (p * (Polynomial.monomial 0) r) d = Polynomial.coeff p d * r
        source
        theorem Polynomial.coeff_monomial_zero_mul {R : Type u} [Semiring R] (p : Polynomial R) (d : ℕ) (r : R) :
        Polynomial.coeff ((Polynomial.monomial 0) r * p) d = r * Polynomial.coeff p d
        source
        theorem Polynomial.mul_X_pow_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (H : p * Polynomial.X ^ n = 0) :
        p = 0
        source
        theorem Polynomial.isRegular_X_pow {R : Type u} [Semiring R] (n : ℕ) :
        IsRegular (Polynomial.X ^ n)
        source
        @[simp]
        theorem Polynomial.isRegular_X {R : Type u} [Semiring R] :
        IsRegular Polynomial.X
        source
        theorem Polynomial.coeff_X_add_C_pow {R : Type u} [Semiring R] (r : R) (n : ℕ) (k : ℕ) :
        Polynomial.coeff ((Polynomial.X + Polynomial.C r) ^ n) k = r ^ (n - k) * ↑(Nat.choose n k)
        source
        theorem Polynomial.coeff_X_add_one_pow (R : Type u_1) [Semiring R] (n : ℕ) (k : ℕ) :
        Polynomial.coeff ((Polynomial.X + 1) ^ n) k = ↑(Nat.choose n k)
        source
        theorem Polynomial.coeff_one_add_X_pow (R : Type u_1) [Semiring R] (n : ℕ) (k : ℕ) :
        Polynomial.coeff ((1 + Polynomial.X) ^ n) k = ↑(Nat.choose n k)
        source
        theorem Polynomial.C_dvd_iff_dvd_coeff {R : Type u} [Semiring R] (r : R) (φ : Polynomial R) :
        Polynomial.C r ∣ φ ↔ ∀ (i : ℕ), r ∣ Polynomial.coeff φ i
        source
        theorem Polynomial.coeff_bit0_mul {R : Type u} [Semiring R] (P : Polynomial R) (Q : Polynomial R) (n : ℕ) :
        Polynomial.coeff (bit0 P * Q) n = 2 * Polynomial.coeff (P * Q) n
        source
        theorem Polynomial.coeff_bit1_mul {R : Type u} [Semiring R] (P : Polynomial R) (Q : Polynomial R) (n : ℕ) :
        Polynomial.coeff (bit1 P * Q) n = 2 * Polynomial.coeff (P * Q) n + Polynomial.coeff Q n
        source
        theorem Polynomial.smul_eq_C_mul {R : Type u} [Semiring R] {p : Polynomial R} (a : R) :
        a • p = Polynomial.C a * p
        source
        theorem Polynomial.update_eq_add_sub_coeff {R : Type u_1} [Ring R] (p : Polynomial R) (n : ℕ) (a : R) :
        Polynomial.update p n a = p + Polynomial.C (a - Polynomial.coeff p n) * Polynomial.X ^ n
        source
        theorem Polynomial.nat_cast_coeff_zero {n : ℕ} {R : Type u_1} [Semiring R] :
        Polynomial.coeff (↑n) 0 = ↑n
        source
        theorem Polynomial.nat_cast_inj {m : ℕ} {n : ℕ} {R : Type u_1} [Semiring R] [CharZero R] :
        ↑m = ↑n ↔ m = n
        source
        @[simp]
        theorem Polynomial.int_cast_coeff_zero {i : ℤ} {R : Type u_1} [Ring R] :
        Polynomial.coeff (↑i) 0 = ↑i
        source
        theorem Polynomial.int_cast_inj {m : ℤ} {n : ℤ} {R : Type u_1} [Ring R] [CharZero R] :
        ↑m = ↑n ↔ m = n
        source
        instance Polynomial.charZero {R : Type u} [Semiring R] [CharZero R] :
        CharZero (Polynomial R)
        Equations