blockDiagonal'_one — Mathlib

English

If each block is the identity matrix, then blockDiagonal' of the identity equals the identity matrix (on the block-structured space).

Русский

Если каждая блок-матрица равна единичной, то блочно-диагональная матрица единична на соответствующей размерности.

LaTeX

$$$ \\mathrm{blockDiagonal}' \\bigl( 1 \\bigr) = 1 $$$

Lean4

@[simp]
theorem blockDiagonal'_one [∀ i, DecidableEq (m' i)] [One α] : blockDiagonal' (1 : ∀ i, Matrix (m' i) (m' i) α) = 1 :=
  show (blockDiagonal' fun i : o => diagonal fun _ : m' i => (1 : α)) = diagonal fun _ => 1 by
    rw [blockDiagonal'_diagonal]

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