English
BlockDiagonal commutes with applying a function entrywise, provided the function preserves zero: map f to the matrix entries commutes with blockDiagonal.
Русский
BlockDiagonal соблюдает отображение по элементам, если функция сохраняет ноль; отображение применяется к блокам поровну.
LaTeX
$$$\operatorname{blockDiagonal}(M)\mapsto f\bigl(\operatorname{blockDiagonal}(M)\bigr) = \operatorname{blockDiagonal}(\lambda k. f(M_k)).$$$
Lean4
@[simp]
theorem blockDiagonal_mul [Fintype n] [Fintype o] [NonUnitalNonAssocSemiring α] (M : o → Matrix m n α)
(N : o → Matrix n p α) : (blockDiagonal fun k => M k * N k) = blockDiagonal M * blockDiagonal N :=
by
ext ⟨i, k⟩ ⟨j, k'⟩
simp only [blockDiagonal_apply, mul_apply, ← Finset.univ_product_univ, Finset.sum_product]
split_ifs with h <;> simp [h]
