English
In a star-algebra context, the conjugate transpose of a block matrix fromBlocks A B C D is obtained blockwise by taking the conjugate transpose of each block in the corresponding positions: (fromBlocks A B C D)ᴴ = fromBlocks Aᴴ Cᴴ Bᴴ Dᴴ.
Русский
В контексте звёздных алгебр сопряжённое транспонирование блочной матрицы fromBlocks A B C D получается по-блочно: (fromBlocks A B C D)ᴴ = fromBlocks Aᴴ Cᴴ Bᴴ Dᴴ.
LaTeX
$$$ (\\text{fromBlocks } A \\ B \\ C \\ D)^{\\dagger} = \\text{fromBlocks } A^{\\dagger} C^{\\dagger} B^{\\dagger} D^{\\dagger} $$$
Lean4
theorem fromBlocks_conjTranspose [Star α] (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
(fromBlocks A B C D)ᴴ = fromBlocks Aᴴ Cᴴ Bᴴ Dᴴ := by simp only [conjTranspose, fromBlocks_transpose, fromBlocks_map]
