Theorems · Definition · linear algebra

Matrix.submatrix

{l : Type u_1} →
  {m : Type u_2} → {n : Type u_3} → {o : Type u_4} → {α : Type v} → Matrix m n α → (l → m) → (o → n) → Matrix l o α

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.

Defined in

Mathlib.LinearAlgebra.Matrix.Defs

Cited by

183 results in Mathlib

Foundations

Depth 14 from the axioms, rests on 61 definitions · uses Quot.sound