length_coeffList_eq_ite — Mathlib

English

With decidable equality on the coefficient ring, the length of coeffList equals 0 if the polynomial is zero, otherwise natDegree + 1.

Русский

При распознанной эквивалентности кольца коэффициентов длина coeffList равна 0, если полином нулевой, иначе deg(p) + 1.

LaTeX

$$$ [DecidableEq R] \\Rightarrow P.c oeffList.length = \\text{if } P = 0 \\text{ then } 0 \\text{ else } P.natDegree + 1 $$$

Lean4

@[simp]
theorem length_coeffList_eq_ite [DecidableEq R] (P : R[X]) :
    P.coeffList.length = if P = 0 then 0 else P.natDegree + 1 := by
  by_cases h : P = 0 <;> simp [h, coeffList, withBotSucc_degree_eq_natDegree_add_one]

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