blockDiagonal_transpose — Mathlib

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

Похожие утверждения