English
Composing a formal multilinear series p with the zero linear map yields a constant formal multilinear series with value equal to p0.
Русский
Сочетание формальной мультилинеарной серии p с нулевым линейным отображением даёт константную формальную серию со значением p0.
LaTeX
$$$ p.compContinuousLinearMap 0 = \\text{constFormalMultilinearSeries } 𝕜 E (p 0 0) $$$
Lean4
@[simp]
theorem compContinuousLinearMap_zero [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
[NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G]
(p : FormalMultilinearSeries 𝕜 F G) :
p.compContinuousLinearMap (0 : E →L[𝕜] F) = constFormalMultilinearSeries 𝕜 E (p 0 0) :=
by
ext n v
cases n with
|
zero =>
simp only [FormalMultilinearSeries.compContinuousLinearMap_apply, Matrix.zero_empty,
constFormalMultilinearSeries_apply_zero, ContinuousMultilinearMap.uncurry0_apply]
congr
apply Subsingleton.allEq
| succ => simp [ContinuousLinearMap.coe_zero']
