blockDiag_transpose — Mathlib

English

Transposing blockDiag M within the k-th block gives the same as taking the transpose of M within the k-th block.

Русский

Транспонирование блока blockDiag M по блоку k эквивалентно транспонированию самого блока M в этом же блоке.

LaTeX

$$$ (blockDiag M^{T})_k = (blockDiag M_k)^{T} $$$

Lean4

@[simp]
theorem blockDiag_transpose (M : Matrix (m × o) (n × o) α) (k : o) : blockDiag Mᵀ k = (blockDiag M k)ᵀ :=
  ext fun _ _ => rfl

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