blockDiagonal_conjTranspose — Mathlib

English

If α has a star-additive structure, then the conjugate transpose of a blockDiagonal matrix is the blockDiagonal of the conjugate transposes of the blocks.

Русский

При наличии структуры звёздочного добавления в α сопряжённая транспозиция блочной диагонали равна блочной диагонали сопряжённых транспонированных блоков.

LaTeX

$$$\bigl(\operatorname{blockDiagonal} M\bigr)^{\mathsf{H}} = \operatorname{blockDiagonal}(M^{\mathsf{H}}).$$$

Lean4

@[simp]
theorem blockDiagonal_conjTranspose {α : Type*} [AddMonoid α] [StarAddMonoid α] (M : o → Matrix m n α) :
    (blockDiagonal M)ᴴ = blockDiagonal fun k => (M k)ᴴ :=
  by
  simp only [conjTranspose, blockDiagonal_transpose]
  rw [blockDiagonal_map _ star (star_zero α)]

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