The executable principal-submatrix and row-prefix operations correspond to Mathlib's Matrix.submatrix reindexed along Fin.castLE.

@[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.