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]