English
Let d be a family of blocks d(i) ∈ Matrix n n R indexed by m. The composition of the block-diagonal matrix given by d equals the reindexed block-diagonal formed from the blocks d(i).
Русский
Пусть d — семейство блоков d(i) ∈ Matrix n n R индексируемое по m. Композиция блочной диагонали, заданной d, равна перенумерованной блочной диагонали, составленной из блоков d(i).
LaTeX
$$$\\operatorname{comp}(\\text{diagonal } d) = (\\text{blockDiagonal } d)^{\\text{reindex}}$$$
Lean4
theorem comp_diagonal (d) : comp m m n n R (diagonal d) = (blockDiagonal d).reindex (.prodComm ..) (.prodComm ..) :=
by
ext
simp [diagonal, blockDiagonal, Matrix.ite_apply]
