English
The id formal multilinear series has only the first coefficient nonzero and the rest zero, with a fixed constant term x.
Русский
Идентити-ряд имеет только первый коэффициент ненулевой, остальные нулевые, фиксированное константное слагаемое x.
LaTeX
$$$\\text{id}(x)\\!\\_n = \\begin{cases} x & n=0, \\\\ \\text{Id} & n=1, \\\\ 0 & n>1. \\end{cases}$$$
Lean4
/-- The identity formal multilinear series, with all coefficients equal to `0` except for `n = 1`
where it is (the continuous multilinear version of) the identity. We allow an arbitrary
constant coefficient `x`. -/
def id (x : E) : FormalMultilinearSeries 𝕜 E E
| 0 => ContinuousMultilinearMap.uncurry0 𝕜 _ x
| 1 => (continuousMultilinearCurryFin1 𝕜 E E).symm (ContinuousLinearMap.id 𝕜 E)
| _ => 0
