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