blockDiag_conjTranspose — Mathlib

English

Block-diagonal extraction commutes with conjugate transpose for matrices with a star structure.

Русский

Извлечение блока, как блочная диагональ, сохраняет сопряженное транспонирование: blockDiag Mᴴ k = (blockDiag M k)ᴴ.

LaTeX

$$$ blockDiag M^{\!H} k = (blockDiag M k)^{\!H} $$$

Lean4

@[simp]
theorem blockDiag_conjTranspose {α : Type*} [Star α] (M : Matrix (m × o) (n × o) α) (k : o) :
    blockDiag Mᴴ k = (blockDiag M k)ᴴ :=
  ext fun _ _ => rfl

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