English
The constant formal multilinear series with value c has degree-zero term equal to c via uncurry0, and all higher-degree terms vanish.
Русский
Константная формальная мультилинеарная серия со значением c имеет степень ноль равной c через uncurry0, а все более высокие степени равны нулю.
LaTeX
$$$ (\text{constFormalMultilinearSeries } 𝕜 E c)(n) = \\begin{cases} \\text{ContinuousMultilinearMap.uncurry0 } 𝕜 E c, & n=0 \\\\ 0, & n>0 \\end{cases} $$$
Lean4
/-- The formal multilinear series where all terms of positive degree are equal to zero, and the term
of degree zero is `c`. It is the power series expansion of the constant function equal to `c`
everywhere. -/
def constFormalMultilinearSeries (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*) [NormedAddCommGroup E]
[NormedSpace 𝕜 E] [ContinuousConstSMul 𝕜 E] [IsTopologicalAddGroup E] {F : Type*} [NormedAddCommGroup F]
[IsTopologicalAddGroup F] [NormedSpace 𝕜 F] [ContinuousConstSMul 𝕜 F] (c : F) : FormalMultilinearSeries 𝕜 E F
| 0 => ContinuousMultilinearMap.uncurry0 _ _ c
| _ => 0
