col_eq_transpose — Mathlib

English

For any matrix A, the column function A.col equals the transpose relation, i.e., A.col j is the vector with entries A(i,j). Equivalently, a column corresponds to the j-th row of A^T.

Русский

Для любой матрицы A функция столбцов удовлетворяет A.col j = (A^T)_{j,·}, то есть столбец формируется как строка транспонированной матрицы.

LaTeX

$$$A.col(j)\text{ is the vector } i \mapsto A_{i j}$, i.e. $A.col j = (A^T)_{j,\cdot}$$$

Lean4

theorem col_eq_transpose (A : Matrix m n α) : A.col = of.symm Aᵀ :=
  rfl

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