trace_blockDiagonal' — Mathlib

English

The variant trace of a block diagonal structure: tr(blockDiagonal' M) = ∑_i tr(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 → Type*} [∀ i, Fintype (m i)] (M : ∀ i, Matrix (m i) (m i) R) :
    trace (blockDiagonal' M) = ∑ i, trace (M i) := by simp [blockDiagonal', trace, Finset.sum_sigma']

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