blockDiag'_blockDiagonal' — Mathlib

English

BlockDiag' distributes over the blockDiagonal' operation in a way that recovers the original block structure: blockDiag'(blockDiagonal' M) = M.

Русский

BlockDiag' распределяется по операции blockDiagonal' так, что восстанавливается исходная блочная структура: blockDiag'(blockDiagonal' M) = M.

LaTeX

$$$ \\mathrm{blockDiag}'( \\mathrm{blockDiagonal}' M ) = M $$$

Lean4

@[simp]
theorem blockDiag'_blockDiagonal' [DecidableEq o] (M : ∀ i, Matrix (m' i) (n' i) α) :
    blockDiag' (blockDiagonal' M) = M :=
  funext fun _ => ext fun _ _ => blockDiagonal'_apply_eq M _ _ _

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