English
Definition: Given a formal multilinear series p indexed by Fin c.length and a vector v: Fin n → E, the function applyOrderedFinpartition p c v maps each block i to p i applied to the coordinates from the i-th block of v.
Русский
Определение: задана последовательность p i и вектор v, функция applyOrderedFinpartition p c v берет i-ю часть и применяет к ней коэффициент p i.
LaTeX
$$$\text{applyOrderedFinpartition}(p,c)(v)(m) = p(m)(v \circ c.emb m)$$$
Lean4
/-- Given a formal multilinear series `p`, an ordered partition `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.applyOrderedFinpartition c v i` for `v : Fin n → E` and `i : Fin c.k`. -/
def applyOrderedFinpartition (p : ∀ (i : Fin c.length), E [×c.partSize i]→L[𝕜] F) : (Fin n → E) → Fin c.length → F :=
fun v m ↦ p m (v ∘ c.emb m)
