comp_coeff_zero'' — Mathlib

English

The general composition of two formal multilinear series is defined by summing over all compositions of n.

Русский

Обобщенная композиция формальных много-линейных рядов задается суммой по всем композициям n.

LaTeX

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

Lean4

/-- The `0`-th coefficient of `q.comp p` is `q 0`. When `p` goes from `E` to `E`, this can be
expressed as a direct equality -/
theorem comp_coeff_zero'' (q : FormalMultilinearSeries 𝕜 E F) (p : FormalMultilinearSeries 𝕜 E E) :
    (q.comp p) 0 = q 0 := by ext v; exact q.comp_coeff_zero p _ _

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