trace_sum — Mathlib

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

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