English
Taking the transpose of a blockDiagonal matrix yields the blockDiagonal of the transposed blocks.
Русский
Сопряженная транспозиция блочной диагонали соответствует блочной диагонали транспонированных блоков.
LaTeX
$$$\bigl(blockDiagonal M\bigr)^T = \operatorname{blockDiagonal}(M^T).$$$
Lean4
@[simp]
theorem blockDiagonal_transpose (M : o → Matrix m n α) : (blockDiagonal M)ᵀ = blockDiagonal fun k => (M k)ᵀ :=
by
ext
simp only [transpose_apply, blockDiagonal_apply, eq_comm]
split_ifs with h
· rw [h]
· rfl