conjTranspose_fromCols_eq_fromRows_conjTranspose

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

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