English
Transposing a matrix partitioned by columns yields a matrix partitioned by rows, whose blocks are the transposes of the original column blocks: transpose(fromCols(A1, A2)) = fromRows(transpose(A1), transpose(A2)).
Русский
Транспонирование матрицы, разбитой по столбцам, дает матрицу, разбитую по строкам, блоки которой являются транспонированными исходными столбцовыми блоками: transpose(fromCols(A1,A2)) = fromRows(transpose(A1), transpose(A2)).
LaTeX
$$$$\operatorname{transpose}\bigl(\operatorname{fromCols}(A_1,A_2)\bigr)=\operatorname{fromRows}(\operatorname{transpose}(A_1))(\operatorname{transpose}(A_2)).$$$$
Lean4
/-- A column partitioned matrix when transposed gives a row partitioned matrix with columns of the
initial matrix transposed to become rows. -/
theorem transpose_fromCols (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
transpose (fromCols A₁ A₂) = fromRows (transpose A₁) (transpose A₂) := by ext (i | i) j <;> simp
