coeff_derivative — Mathlib

English

For a power-series f, the n-th coefficient of its derivative equals (n+1) times the coefficient of f at index n+1: coeff_n(f') = (n+1) coeff_{n+1}(f).

Русский

Для степенного ряда f коэффициент н производной равен (н+1) умножить на коэффициент f с индексом n+1: coeff_n(f') = (n+1) coeff_{n+1}(f).

LaTeX

$$$ \\operatorname{coeff}_n( \\mathrm{d}/\\mathrm{d}X\, f) = (n+1) \\operatorname{coeff}_{n+1}(f) $$$

Lean4

theorem coeff_derivative (f : R⟦X⟧) (n : ℕ) : coeff n (d⁄dX R f) = coeff (n + 1) f * (n + 1) :=
  coeff_derivativeFun f n

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