trace_blockDiagonal — Mathlib

English

If M is a family of matrices M_i, then tr(blockDiagonal M) = ∑_i tr(M_i).

Русский

Если M — семья матриц M_i, то tr(blockDiagonal M) = ∑_i tr(M_i).

LaTeX

$$$$ \operatorname{tr}( \operatorname{blockDiagonal} M ) = \sum_i \operatorname{tr}(M_i) $$$$

Lean4

theorem trace_blockDiagonal [DecidableEq p] (M : p → Matrix n n R) : trace (blockDiagonal M) = ∑ i, trace (M i) := by
  simp [blockDiagonal, trace, Finset.sum_comm (γ := n), Fintype.sum_prod_type]

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