English
The zero-th coefficient of q.comp p is equal to q0 applied to the zero inputs, consistent across spaces.
Русский
Нулевой коэффициент q.comp p равен q0 на нулевых входах, сохраняется при любом выборе пространств.
LaTeX
$$$(q.comp p) 0 = q 0$ on zero-input vectors.$$
Lean4
/-- The first coefficient of a composition of formal multilinear series is the composition of the
first coefficients seen as continuous linear maps. -/
theorem comp_coeff_one (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (v : Fin 1 → E) :
(q.comp p) 1 v = q 1 fun _i => p 1 v :=
by
have : {Composition.ones 1} = (Finset.univ : Finset (Composition 1)) :=
Finset.eq_univ_of_card _ (by simp [composition_card])
simp only [FormalMultilinearSeries.comp, compAlongComposition_apply, ← this, Finset.sum_singleton]
refine q.congr (by simp) fun i hi1 hi2 => ?_
simp only [applyComposition_ones]
exact p.congr rfl fun j _hj1 hj2 => by congr!
