English
Symmetry of the diagonal under conjugate transpose across blocks: conjTranspose(diagonal d) equals diagonal of conjTranspose blocks.
Русский
Симметрия диагонали при сопряжённо-транспонировании по блокам: conjTranspose(diagonal d) = diagonal(conjTranspose A1, conjTranspose A2).
LaTeX
$$$ \operatorname{conjTranspose}(\mathrm{diagonal}(d)) = \mathrm{diagonal}( \mathrm{conjTranspose}(\text{block}_1), \mathrm{conjTranspose}(\text{block}_2) ) $$$
Lean4
@[simp]
theorem comp_symm_diagonal [DecidableEq I] [DecidableEq J] [Zero R] (d : I × J → R) :
(comp I I J J R).symm (diagonal d) = diagonal fun i => diagonal fun j => d (i, j) :=
(comp I I J J R).symm_apply_eq.2 <| (comp_diagonal_diagonal fun i j => d (i, j)).symm
