English
For an m × n matrix A, A.col j is the j-th column regarded as a vector in m → α; equivalently, (A.col j)(i) = A(i,j) for all i ∈ m, j ∈ n.
Русский
Для матрицы размером m × n функция A.col j представляет j-й столбец как вектор в m → α; тождественно (A.col j)(i) = A(i,j).
LaTeX
$$$(A.col j)(i) = A_{i j}$ for all $i \in \{0,\dots,m-1\},\ j \in \{0,\dots,n-1\}$$$
Lean4
/-- For an `m × n` `α`-matrix `A`, `A.col j` is the `j`th column of `A` as a vector in `m → α`.
`A.col` is defeq to `Aᵀ`, but refers to the 'column function' of `A`
while avoiding defeq abuse and noisy eta-expansions
(and without the simplifier unfolding transposes) in expressions like `Set.Injective A.col`
and `Set.range A.col`.
(Note 2025-04-07 : the identifier `Matrix.col` used to refer to a matrix with all columns equal;
this is now called `Matrix.replicateCol`) -/
def col (A : Matrix m n α) : n → m → α :=
Aᵀ
