English
For a multilinear map f, and given a finite index set t, the value on a piecewise-defined sum is the sum over all subsets of t of the values on the corresponding piecewise arguments.
Русский
Для мультиленейной карты f и конечного множества t, значение на разложении по кускам равно сумме по всем подмножествам t значений на соответствующих кусочных аргументах.
LaTeX
$$$ f (t.piecewise (m + m') m') = \\sum_{s \\subseteq t} f (s.piecewise m m') $$$
Lean4
/-- Additivity of a multilinear map along all coordinates at the same time,
writing `f (m + m')` as the sum of `f (s.piecewise m m')` over all sets `s`. -/
theorem map_add_univ [DecidableEq ι] [Fintype ι] (m m' : ∀ i, M₁ i) :
f (m + m') = ∑ s : Finset ι, f (s.piecewise m m') := by simpa using f.map_piecewise_add m m' Finset.univ
