leadingCoeff_taylor — Mathlib

English

Let R be a semiring and f ∈ R[X]. For any r ∈ R, the leading coefficient of the Taylor expansion of f around r is the same as the leading coefficient of f.

Русский

Пусть R — полукольцо и f ∈ R[X]. Для любого r ∈ R старший коэффициент ряда Тейлора taylor(r, f) равен старшему коэффициенту f.

LaTeX

$$$$ \\operatorname{leadingCoeff}(\\operatorname{taylor}(r,f)) = \\operatorname{leadingCoeff}(f). $$$$

Lean4

@[simp]
theorem leadingCoeff_taylor : (taylor r f).leadingCoeff = f.leadingCoeff := by
  rw [leadingCoeff, leadingCoeff, natDegree_taylor, coeff_taylor_natDegree, leadingCoeff]

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