English
The first coefficient of a composition q.compAlongComposition p equals the composition of the first coefficients q1 and p1.
Русский
Первый коэффициент композиции q.compAlongComposition p равен композиции первых коэффициентов q1 и p1.
LaTeX
$$$(q.compAlongComposition p\\, c) = q(1)\\circ p(1)$ for the case n=1; more generally, the theorem states the equality of the first coefficients.$$
Lean4
/-- The `0`-th coefficient of `q.comp p` is `q 0`. Since these maps are multilinear maps in zero
variables, but on different spaces, we cannot state this directly, so we state it when applied to
arbitrary vectors (which have to be the zero vector). -/
theorem comp_coeff_zero (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (v : Fin 0 → E)
(v' : Fin 0 → F) : (q.comp p) 0 v = q 0 v' :=
by
let c : Composition 0 := Composition.ones 0
dsimp [FormalMultilinearSeries.comp]
have : { c } = (Finset.univ : Finset (Composition 0)) := by
apply Finset.eq_of_subset_of_card_le <;> simp [Finset.card_univ, composition_card 0]
rw [← this, Finset.sum_singleton, compAlongComposition_apply]
symm; congr!
