English
The map taking a family of matrices to its blockDiagonal commutes with maps applied entrywise, up to the corresponding zero condition on the images of 0.
Русский
Отображение, переводящее семью матриц в блочную диагональ, согласуется с приложением функции к каждому блоку поэлементно, когда сохраняется условие отображения нуля в ноль.
LaTeX
$$$\bigl(blockDiagonal M\bigr) \mapsto f\bigl( blockDiagonal M \bigr) = blockDiagonal\bigl( M \mapsto fM \bigr)$$$
Lean4
theorem blockDiagonal_map (M : o → Matrix m n α) (f : α → β) (hf : f 0 = 0) :
(blockDiagonal M).map f = blockDiagonal fun k => (M k).map f :=
by
ext
simp only [map_apply, blockDiagonal_apply]
rw [apply_ite f, hf]
