English
For a finite index set s and a family f, tr(∑_{i∈s} f(i)) = ∑_{i∈s} tr(f(i)).
Русский
Для конечного множества индексов s и семейства f выполняется tr(∑_{i∈s} f(i)) = ∑_{i∈s} tr(f(i)).
LaTeX
$$$$ \operatorname{tr}\left( \sum_{i \in s} f(i) \right) = \sum_{i \in s} \operatorname{tr}(f(i)) $$$$
Lean4
@[simp]
theorem trace_sum (s : Finset ι) (f : ι → Matrix n n R) : trace (∑ i ∈ s, f i) = ∑ i ∈ s, trace (f i) :=
map_sum (traceAddMonoidHom n R) f s