coeff_taylor_natDegree — Mathlib

English

The coefficient at f.natDegree equals the leading coefficient of f.

Русский

Коэффициент при степени f.natDegree равен ведущему коэффициенту f.

LaTeX

$$$$ (\operatorname{taylor} r f)_{f.natDegree} = f^{\mathrm{leadingCoeff}} $$$$

Lean4

@[simp]
theorem coeff_taylor_natDegree : (taylor r f).coeff f.natDegree = f.leadingCoeff :=
  by
  by_cases hf : f = 0
  · rw [hf, map_zero, coeff_natDegree]
  · rw [taylor_coeff, hasseDeriv_natDegree_eq_C, eval_C]

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