coeffList_eq_cons_leadingCoeff — Mathlib

English

If P ≠ 0, then P.coeffList starts with the leading coefficient P.leadingCoeff; i.e., P.coeffList = (P.leadingCoeff) :: ls for some list ls.

Русский

Если P ≠ 0, то coeffList(P) начинается с ведущего коэффициента P.leadingCoeff; то есть P.coeffList = P.leadingCoeff :: ls для некоторого списка ls.

LaTeX

$$$ P \\neq 0 \\Rightarrow \\exists ls,\\; P.coeffList = P.leadingCoeff :: ls $$$

Lean4

theorem coeffList_eq_cons_leadingCoeff (h : P ≠ 0) : ∃ ls, P.coeffList = P.leadingCoeff :: ls := by
  simp [coeffList, List.range_succ, withBotSucc_degree_eq_natDegree_add_one h]

Похожие утверждения