decompose_symm_sum — Mathlib

English

For any Finset ι' and f: ι' → DirectSum, the symm of the finite sum equals the sum of symms: (decompose ℳ).symm (∑ f i) = ∑ (decompose ℳ).symm (f i).

Русский

Для любого конечного множества ι' и отображения f: ι' → DirectSum, симметрическое отображение суммы равно сумме симметрий.

LaTeX

$$$\forall s, \sum_{i\in s} (\mathrm{decompose}_{\mathcal{M}})^{-1}(f(i)) = (\mathrm{decompose}_{\mathcal{M}})^{-1}\left(\sum_{i\in s} f(i)\right)$$$

Lean4

@[simp]
theorem decompose_symm_sum {ι'} (s : Finset ι') (f : ι' → ⨁ i, ℳ i) :
    (decompose ℳ).symm (∑ i ∈ s, f i) = ∑ i ∈ s, (decompose ℳ).symm (f i) :=
  map_sum (decomposeAddEquiv ℳ).symm f s

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