blockDiagonal_apply_eq — Mathlib

English

If d assigns a diagonal matrix to each block, blockDiagonal of these diagonals equals the overall diagonal formed from the blocks.

Русский

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

LaTeX

$$$\operatorname{blockDiagonal} \bigl(\mathrm{diagonal}(d(k))\bigr) = \mathrm{diagonal}(d(k))$$$

Lean4

@[simp]
theorem blockDiagonal_apply_eq (M : o → Matrix m n α) (i j k) : blockDiagonal M (i, k) (j, k) = M k i j :=
  if_pos rfl

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