English
In a star ring, taking the conjugate transpose distributes over block partitioning: conjTranspose(fromCols A1 A2) = fromRows (conjTranspose A1) (conjTranspose A2).
Русский
В кольце со звездой сопряженно-транспонирование распределяется по блочному разбиению: conjTranspose(fromCols A1 A2) = fromRows(conjTranspose A1) (conjTranspose A2).
LaTeX
$$$ \operatorname{conjTranspose}(\mathrm{fromCols}(A_1,A_2)) = \mathrm{fromRows}(\operatorname{conjTranspose}(A_1)) (\operatorname{conjTranspose}(A_2)) $$$
Lean4
/-- A column partitioned matrix in a Star ring when conjugate transposed gives a row partitioned
matrix with the columns of the initial matrix conjugate transposed to become rows. -/
theorem conjTranspose_fromCols_eq_fromRows_conjTranspose (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
conjTranspose (fromCols A₁ A₂) = fromRows (conjTranspose A₁) (conjTranspose A₂) := by ext (_ | _) _ <;> simp