constFormalMultilinearSeries_apply_zero

English

The zero-degree term of constFormalMultilinearSeries equals uncurry0: constFormalMultilinearSeries 𝕜 E c 0 = ContinuousMultilinearMap.uncurry0 𝕜 E c.

Русский

Нулевой член константной формальной серии равен uncurry0: constFormalMultilinearSeries 𝕜 E c 0 = ContinuousMultilinearMap.uncurry0 𝕜 E c.

LaTeX

$$$ constFormalMultilinearSeries 𝕜 E c 0 = \\text{ContinuousMultilinearMap.uncurry0 } 𝕜 E c $$$

Lean4

@[simp]
theorem constFormalMultilinearSeries_apply_zero [NontriviallyNormedField 𝕜] [NormedAddCommGroup E]
    [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {c : F} :
    constFormalMultilinearSeries 𝕜 E c 0 = ContinuousMultilinearMap.uncurry0 _ _ c :=
  rfl

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