derivSeries_coeff_one — Mathlib

English

The coeff of the derivative series for p at n, evaluated at vector 1, equals (n+1) times p(n+1).

Русский

Коэффициент производной ряда в позиции n, при векторе 1, равен (n+1) p(n+1).

LaTeX

$$$p.derivSeries.coeff\ n\ 1 = (n+1) \cdot p(n+1).$$$

Lean4

@[simp]
theorem derivSeries_coeff_one (p : FormalMultilinearSeries 𝕜 𝕜 F) (n : ℕ) :
    p.derivSeries.coeff n 1 = (n + 1) • p.coeff (n + 1) :=
  p.derivSeries_apply_diag _ _

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