English
For any formal multilinear series p and natural n, composing with the all-ones composition reduces to applying the first-order coefficient: the n-th block behaves as if using coefficient p1.
Русский
Для любой формальной многолинейной серии p и натурального n композиция по всем единицам сводит к применению первого коэффициента: n-й блок ведет себя как если бы использовал коэффициент p1.
LaTeX
$$$p.applyComposition(\\mathrm{Composition.ones\\}n) = \\lambda v,i.\\; p(1) (\\text{(применение к }v\\text{ в i-том блоке)})$$$
Lean4
/-- Given a formal multilinear series `p`, a composition `c` of `n` and the index `i` of a
block of `c`, we may define a function on `Fin n → E` by picking the variables in the `i`-th block
of `n`, and applying the corresponding coefficient of `p` to these variables. This function is
called `p.applyComposition c v i` for `v : Fin n → E` and `i : Fin c.length`. -/
def applyComposition (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (c : Composition n) : (Fin n → E) → Fin c.length → F :=
fun v i => p (c.blocksFun i) (v ∘ c.embedding i)
