English
Given a matrix A with row index m, column index n, and maps r:l→m, c:o→n, the submatrix A.submatrix r c is the matrix with entries (A.submatrix r c)_{i j} = A_{r(i), c(j)}.
Русский
У данной матрицы A с индексами строк m и столбцов n есть подматрица A.submatrix r c, чьи элементы удовлетворяют (A.submatrix r c)_{i j} = A_{r(i), c(j)}.
LaTeX
$$$ (A.submatrix\ r\ c)_{ij} = A_{r(i),\ c(j)} $$$
Lean4
/-- Given maps `(r : l → m)` and `(c : o → n)` reindexing the rows and columns of
a matrix `M : Matrix m n α`, the matrix `M.submatrix r c : Matrix l o α` is defined
by `(M.submatrix r c) i j = M (r i) (c j)` for `(i,j) : l × o`.
Note that the total number of row and columns does not have to be preserved. -/
def submatrix (A : Matrix m n α) (r : l → m) (c : o → n) : Matrix l o α :=
of fun i j => A (r i) (c j)
