head_coeffList — Mathlib

English

The head of the coefficient list of P is the leading coefficient of P when P ≠ 0.

Русский

Глава списка коэффициентов P равна ведущему коэффициенту P при P ≠ 0.

LaTeX

$$$ head\\_coeffList (P) = P.leadingCoeff \\quad \\text{for } P \\neq 0 $$$

Lean4

@[simp]
theorem head_coeffList (P : R[X]) (hP) : P.coeffList.head hP = P.leadingCoeff :=
  let h := coeffList_eq_nil.not.mp hP
  (coeffList_eq_cons_leadingCoeff h).casesOn fun _ _ ↦ Option.some.injEq _ _ ▸ List.head?_eq_head _ ▸ head?_coeffList h

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