A list of coefficients of a polynomial

Definition

• coeffList f: a List of the coefficients, from leading term down to constant term.
• coeffList 0 is defined to be [].

This is useful for talking about polynomials in terms of list operations. It is "redundant" data in the sense that Polynomial is already a Finsupp (of its coefficients), and Polynomial.coeff turns this into a function, and these have exactly the same data as coeffList. The difference is that coeffList is intended for working together with list operations: getting List.head, comparing adjacent coefficients with each other, or anything that involves induction on Polynomials by dropping the leading term (which is Polynomial.eraseLead).

Note that coeffList starts with the highest-degree terms and ends with the constant term. This might seem backwards in the sense that Polynomial.coeff and List.get! are reversed to one another, but it means that induction on Lists is the same as induction on Polynomial.leadingCoeff.

The most significant theorem here is coeffList_eraseLead, which says that coeffList P can be written as leadingCoeff P :: List.replicate k 0 ++ coeffList P.eraseLead. That is, the list of coefficients starts with the leading coefficient, followed by some number of zeros, and then the coefficients of P.eraseLead.

def Polynomial.coeffList {R : Type u_1} [Semiring R] (P : Polynomial R) : List R

The list of coefficients starting from the leading term down to the constant term.

Equations

• P.coeffList = List.map P.coeff (List.range P.degree.succ).reverse

@[simp]

theorem Polynomial.coeffList_zero (R : Type u_1) [Semiring R] : coeffList 0 = []

@[simp]

theorem Polynomial.coeffList_eq_nil {R : Type u_1} [Semiring R] {P : Polynomial R} : P.coeffList = [] ↔ P = 0

Only the zero polynomial has no coefficients.

@[simp]

theorem Polynomial.coeffList_C {R : Type u_1} [Semiring R] {x : R} (h : x ≠ 0) : (C x).coeffList = [x]

theorem Polynomial.coeffList_eq_cons_leadingCoeff {R : Type u_1} [Semiring R] {P : Polynomial R} (h : P ≠ 0) : ∃ (ls : List R), P.coeffList = P.leadingCoeff :: ls

@[simp]

theorem Polynomial.head?_coeffList {R : Type u_1} [Semiring R] {P : Polynomial R} (h : P ≠ 0) : P.coeffList.head? = some P.leadingCoeff

@[simp]

theorem Polynomial.head_coeffList {R : Type u_1} [Semiring R] (P : Polynomial R) (hP : P.coeffList ≠ []) : P.coeffList.head hP = P.leadingCoeff

theorem Polynomial.length_coeffList_eq_withBotSucc_degree {R : Type u_1} [Semiring R] (P : Polynomial R) : P.coeffList.length = P.degree.succ

@[simp]

theorem Polynomial.length_coeffList_eq_ite {R : Type u_1} [Semiring R] [DecidableEq R] (P : Polynomial R) : P.coeffList.length = if P = 0 then 0 else P.natDegree + 1

theorem Polynomial.leadingCoeff_cons_eraseLead {R : Type u_1} [Semiring R] {P : Polynomial R} (h : P.nextCoeff ≠ 0) : P.leadingCoeff :: P.eraseLead.coeffList = P.coeffList

@[simp]

theorem Polynomial.coeffList_monomial {R : Type u_1} [Semiring R] {x : R} (hx : x ≠ 0) (n : ℕ) : ((monomial n) x).coeffList = x :: List.replicate n 0

theorem Polynomial.coeffList_eraseLead {R : Type u_1} [Semiring R] {P : Polynomial R} (h : P ≠ 0) : P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)

@[simp]

theorem Polynomial.coeffList_neg {R : Type u_1} [Ring R] (P : Polynomial R) : (-P).coeffList = List.map (fun (x : R) => -x) P.coeffList

theorem Polynomial.coeffList_C_mul {R : Type u_1} [DivisionSemiring R] (P : Polynomial R) {x : R} (hx : x ≠ 0) : (C x * P).coeffList = List.map (fun (x_1 : R) => x * x_1) P.coeffList