blockDiag'_conjTranspose — Mathlib

English

BlockDiag' commutes with conjugate transpose: blockDiag' Mᴴ k = (blockDiag' M k)ᴴ.

Русский

BlockDiag' сохраняет сопряжение: blockDiag' Mᴴ k = (blockDiag' M k)ᴴ.

LaTeX

$$$ \\mathrm{blockDiag}' M^{\\dagger} k = (\\mathrm{blockDiag}' M k)^{\\dagger} $$$

Lean4

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

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