blockDiagonal_diagonal — Mathlib

English

If you take blockDiagonal of diagonals, you obtain a diagonal matrix whose entries are the corresponding entries from the blocks.

Русский

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

LaTeX

$$$\operatorname{blockDiagonal}(\lambda k. \operatorname{diagonal}(d_k)) = \operatorname{diagonal}(k \mapsto d_k(k)).$$$

Lean4

@[simp]
theorem blockDiagonal_diagonal [DecidableEq m] (d : o → m → α) :
    (blockDiagonal fun k => diagonal (d k)) = diagonal fun ik => d ik.2 ik.1 :=
  by
  ext ⟨i, k⟩ ⟨j, k'⟩
  simp only [blockDiagonal_apply, diagonal_apply, Prod.mk_inj, ← ite_and]
  congr 1
  rw [and_comm]

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