English
Transposing blockDiagonal' equals blockDiagonal' of transposed M.
Русский
Транспонирование blockDiagonal' эквивалентно блочной диагонали транспонированного M.
LaTeX
$$$ (blockDiagonal' M)^T = blockDiagonal' (k \mapsto M_k)^T $$$
Lean4
theorem blockDiagonal'_map (M : ∀ i, Matrix (m' i) (n' i) α) (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_dite f, hf]