head?_coeffList — Mathlib

English

For a nonzero polynomial P, the leading coefficient equals the head of the coefficient list.

Русский

Для ненулевого P ведущий коэффициент равен голове списка коэффициентов.

LaTeX

$$$ P \\neq 0 \\Rightarrow P.coeffList.head? = \\text{Some}(P.leadingCoeff) $$$

Lean4

@[simp]
theorem head?_coeffList (h : P ≠ 0) : P.coeffList.head? = P.leadingCoeff :=
  (coeffList_eq_cons_leadingCoeff h).casesOn fun _ ↦ (Eq.symm · ▸ rfl)

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