col_transpose — Mathlib

English

For any matrix A, transposition swaps rows with columns; equivalently, the i-th column of A^T equals the i-th row of A, i.e. A^T.col = A.row.

Русский

Для любой матрицы A транспонирование меняет строки на столбцы; эквивалентно тому, что i-й столбец A^T равен i-й строке A, то есть A^T.col = A.row.

LaTeX

$$$A^{\\top}.\\mathrm{col} = A.\\mathrm{row}$$$

Lean4

@[simp]
theorem col_transpose (A : Matrix m n α) : Aᵀ.col = A.row :=
  rfl

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