constFormalMultilinearSeries_apply_succ

English

For any natural n, the (n+1)-st term of constFormalMultilinearSeries is zero: constFormalMultilinearSeries 𝕜 E c (n+1) = 0.

Русский

Для любого натурального n степенный член (n+1) равен нулю: constFormalMultilinearSeries 𝕜 E c (n+1) = 0.

LaTeX

$$$ constFormalMultilinearSeries 𝕜 E c (n + 1) = 0 $$$

Lean4

@[simp]
theorem constFormalMultilinearSeries_apply_succ [NontriviallyNormedField 𝕜] [NormedAddCommGroup E]
    [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {c : F} {n : ℕ} :
    constFormalMultilinearSeries 𝕜 E c (n + 1) = 0 :=
  rfl

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