English
For an m × n matrix A, A.row i is the i-th row viewed as a vector in n → α; equivalently, (A.row i)(j) = A(i,j) for all i ∈ m, j ∈ n.
Русский
Для матрицы размером m × n функция A.row i представляет i‑ю строку как вектор в n → α; тождественно (A.row i)(j) = A(i,j) для всех i ∈ m, j ∈ n.
LaTeX
$$$(A.row i)(j) = 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.row i` is the `i`th row of `A` as a vector in `n → α`.
`A.row` is defeq to `A`, but explicitly refers to the 'row function' of `A`
while avoiding defeq abuse and noisy eta-expansions,
such as in expressions like `Set.Injective A.row` and `Set.range A.row`.
(Note 2025-04-07 : the identifier `Matrix.row` used to refer to a matrix with all rows equal;
this is now called `Matrix.replicateRow`) -/
def row (A : Matrix m n α) : m → n → α :=
A
