English
The id formal multilinear series is the identity in the sense that its nonzero coefficients are exactly the identity maps in degree 1, with a fixed constant term x.
Русский
Идентити-ряд — это тождественный ряд: коэффициент единицы равен тождественному отображению, а остальные нулевые, кроме свободного константного слагаемого.
LaTeX
$$$\\text{id}_{\\mathbb{K},E} =\\begin{cases} x & n=0, \\\\ \\text{Id} & n=1, \\\\ 0 & n>1.\\end{cases}$$$
Lean4
/-- Only `0`-th coefficient of `q.comp p` depends on `q 0`. -/
theorem removeZero_comp_of_pos (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}
(hn : 0 < n) : q.removeZero.comp p n = q.comp p n := by
ext v
simp only [FormalMultilinearSeries.comp, compAlongComposition, ContinuousMultilinearMap.compAlongComposition_apply,
ContinuousMultilinearMap.sum_apply]
refine Finset.sum_congr rfl fun c _hc => ?_
rw [removeZero_of_pos _ (c.length_pos_of_pos hn)]
