@[simp]

theorem HexMatrixMathlib.matrixEquiv_principalSubmatrix {R : Type u} {n : ℕ} (M : Hex.Matrix R n n) (k : ℕ) (hk : k ≤ n) : matrixEquiv (M.principalSubmatrix k hk) = (matrixEquiv M).submatrix (Fin.castLE hk) (Fin.castLE hk)

The k × k principal submatrix is the Fin.castLE-reindexed submatrix.

@[simp]

theorem HexMatrixMathlib.matrixEquiv_takeRows {R : Type u} {n m : ℕ} (M : Hex.Matrix R n m) (k : ℕ) (hk : k ≤ n) : matrixEquiv (M.takeRows k hk) = (matrixEquiv M).submatrix (Fin.castLE hk) id

The first-k-rows slice is the submatrix reindexing rows by Fin.castLE.

@[simp]

theorem HexMatrixMathlib.matrixEquiv_selectRows {R : Type u} {n m k : ℕ} (M : Hex.Matrix R n m) (rows : Vector (Fin n) k) : matrixEquiv (M.selectRows rows) = (matrixEquiv M).submatrix rows.get id

Selecting rows is the submatrix reindexing rows by the index vector.

@[simp]

theorem HexMatrixMathlib.matrixEquiv_selectCols {R : Type u} {n m k : ℕ} (M : Hex.Matrix R n m) (cols : Vector (Fin m) k) : matrixEquiv (M.selectCols cols) = (matrixEquiv M).submatrix id cols.get

Selecting columns is the submatrix reindexing columns by the index vector.