fpowerSeries_apply_add_two

Mathlib.Analysis.Calculus.FormalMultilinearSeries

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.fpowerSeries_apply_add_two

English

The kth iterate of fslope applied to p has nth coefficient equal to p.coeff(n+k).

Русский

k-й итератив FSlope применён к p имеет n-й коэффициент равный p.coeff(n+k).

LaTeX

$$$ (fslope^{[k]} p).coeff n = p.coeff (n + k) $$$

Lean4

@[simp]
theorem fpowerSeries_apply_add_two (f : E →L[𝕜] F) (x : E) (n : ℕ) : f.fpowerSeries x (n + 2) = 0 :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru