conjTranspose_fromRows_eq_fromCols_conjTranspose

English

Similarly, conjTranspose(fromRows A1 A2) = fromCols (conjTranspose A1) (conjTranspose A2).

Русский

Аналогично, conjTranspose(fromRows A1 A2) = fromCols (conjTranspose A1) (conjTranspose A2).

LaTeX

$$$ \operatorname{conjTranspose}(\mathrm{fromRows}(A_1,A_2)) = \mathrm{fromCols}(\operatorname{conjTranspose}(A_1)) (\operatorname{conjTranspose}(A_2)) $$$

Lean4

/-- A row partitioned matrix in a Star ring when conjugate transposed gives a column partitioned
matrix with the rows of the initial matrix conjugate transposed to become columns. -/
theorem conjTranspose_fromRows_eq_fromCols_conjTranspose (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
    conjTranspose (fromRows A₁ A₂) = fromCols (conjTranspose A₁) (conjTranspose A₂) := by ext _ (_ | _) <;> simp

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