Commit 2025-04-02 17:23 80f036f5

View on Github →

feat: Polynomial.coeffList (#9085) Polynomial.coeffList is the list of coefficients, in descending order from leading term to constant term. (The zero polynomial has coeffList of []). The PR defines coeffList and proves some basic facts, notably relating P.coeffList to P.eraseLead.coeffList.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/SuccPred.lean

added theorem Order.succ_eq_zero

Modified Mathlib/Algebra/Polynomial/Coeff.lean

Created Mathlib/Algebra/Polynomial/CoeffList.lean

added def Polynomial.coeffList

added theorem Polynomial.coeffList_C

added theorem Polynomial.coeffList_C_mul

added theorem Polynomial.coeffList_eq_cons_leadingCoeff

added theorem Polynomial.coeffList_eq_nil

added theorem Polynomial.coeffList_eraseLead

added theorem Polynomial.coeffList_monomial

added theorem Polynomial.coeffList_neg

added theorem Polynomial.coeffList_zero

added theorem Polynomial.head?_coeffList

added theorem Polynomial.head_coeffList

added theorem Polynomial.leadingCoeff_cons_eraseLead

added theorem Polynomial.length_coeffList_eq_ite

added theorem Polynomial.length_coeffList_eq_withBotSucc_degree

Modified Mathlib/Algebra/Polynomial/Degree/Definitions.lean

added theorem Polynomial.withBotSucc_degree_eq_natDegree_add_one

Modified Mathlib/Data/Nat/SuccPred.lean

added theorem withBotSucc_one

added theorem withBotSucc_zero

Modified Mathlib/Order/SuccPred/WithBot.lean

added theorem WithBot.succ_eq_bot

added theorem WithTop.pred_eq_top