decompose_symm_add — Mathlib

English

For a finite index set ι' and a function f: ι' → M, the decomposition distributes over finite sums: decompose(∑ f i) = ∑ decompose(f i).

Русский

Разложение распределяется по конечной сумме: decompose(∑ f(i)) = ∑ decompose(f(i)).

LaTeX

$$$\mathrm{decompose}_{\mathcal{M}}\Big(\sum_{i\in s} f(i)\Big) = \sum_{i\in s} \mathrm{decompose}_{\mathcal{M}}(f(i))$$$

Lean4

@[simp]
theorem decompose_symm_add (x y : ⨁ i, ℳ i) :
    (decompose ℳ).symm (x + y) = (decompose ℳ).symm x + (decompose ℳ).symm y :=
  map_add (decomposeAddEquiv ℳ).symm x y

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