English
Let {M_i} be a family of matrices with entries in α, where α is an AddMonoid equipped with a star operation. Then the conjugate transpose of the block diagonal matrix formed from M equals the block diagonal matrix formed from the conjugate transposes of each M_i.
Русский
Пусть дано семейство матриц M_i со значениями из α, где α — аддитивная моноидальная структура с операцией сопряжения. Тогда сопряжённо-транспонированная блочно-диагональная матрица, полученная из M, равна блочно-диагональной матрице, состоящей из сопряжённых транспонированных M_i.
LaTeX
$$$ \\bigl( \\mathrm{blockDiagonal}' M \\bigr)^{*} = \\mathrm{blockDiagonal}' \\bigl( \\lambda k. (M\\,k)^{*} \\bigr) $$$
Lean4
@[simp]
theorem blockDiagonal'_conjTranspose {α} [AddMonoid α] [StarAddMonoid α] (M : ∀ i, Matrix (m' i) (n' i) α) :
(blockDiagonal' M)ᴴ = blockDiagonal' fun k => (M k)ᴴ :=
by
simp only [conjTranspose, blockDiagonal'_transpose]
exact blockDiagonal'_map _ star (star_zero α)
