compAlongComposition_apply — Mathlib

English

Let q, p be formal multilinear series. Define q.compAlongComposition p c by applying p to the appropriate blocks of input and then applying the corresponding coefficient of q.

Русский

Пусть q, p — формальные много-линейные ряды. Определим q.compAlongComposition p c, применяя p к соответствующим блокам входа, затем выбирая соответствующий коэффициент q.

LaTeX

$$$(q\\,\\text{compAlongComposition}\\ p\\ c) = f\\,\\text{with blocks: } f= q_{c.length} \\circOn\\ldots$$$

Lean4

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

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