compAlongComposition_apply — Mathlib

English

For q and p, and a composition c of n, the coefficient (q.compAlongComposition p) is a multilinear map formed by summing the appropriate blocks of q along with p.

Русский

Для q и p и композиции c над n коэффициент (q.compAlongComposition p) является много-линейным отображением, получаемым суммированием соответствующих блоков q вместе с p.

LaTeX

$$$(q.comp p)(n) = \\sum_{c:\\mathrm{Composition}(n)} q.compAlongComposition p c$$$

Lean4

@[simp]
theorem compAlongComposition_apply {n : ℕ} (p : FormalMultilinearSeries 𝕜 E F) (c : Composition n)
    (f : F [×c.length]→L[𝕜] G) (v : Fin n → E) : (f.compAlongComposition p c) v = f (p.applyComposition c v) :=
  rfl

Похожие утверждения