derivSeries — Mathlib

English

If the (n+1)-st coefficient is zero, then the n-th derivative series is identically zero.

Русский

Если коэффициент при n+1-м равно нулю, то n-й ряд производной нулевой.

LaTeX

$$$p( n+1 ) = 0 \\Rightarrow p.derivSeries n = 0$$$

Lean4

/-- `derivSeries p` is a power series for `fderiv 𝕜 f` if `p` is a power series for `f`,
see `HasFPowerSeriesOnBall.fderiv`. -/
def derivSeries : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F) :=
  (continuousMultilinearCurryFin1 𝕜 E F : (E [×1]→L[𝕜] F) →L[𝕜] E →L[𝕜] F) |>.compFormalMultilinearSeries
    (p.changeOriginSeries 1)

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