Principal submatrices and row prefixes.

def Hex.Matrix.principalSubmatrix {R : Type u_1} {n : Nat} (M : Matrix R n n) (k : Nat) (hk : k ≤ n) : Matrix R k k

Leading principal k × k submatrix of a square matrix: the top-left block indexed by {0, …, k-1} along both axes. Includes the empty submatrix (k = 0) and is convenient for Bareiss pivot/minor statements.

Equations

• M.principalSubmatrix k hk = Hex.Matrix.ofFn fun (i j : Fin k) => have ii := ⟨↑i, ⋯⟩; have jj := ⟨↑j, ⋯⟩; M[(ii, jj)]

def Hex.Matrix.takeRows {R : Type u_1} {n m : Nat} (M : Matrix R n m) (k : Nat) (hk : k ≤ n) : Matrix R k m

The first k rows of a matrix, retaining all source columns.

Equations

• M.takeRows k hk = Hex.Matrix.ofFn fun (i : Fin k) (j : Fin m) => have ii := ⟨↑i, ⋯⟩; M[(ii, j)]

theorem Hex.Matrix.getElem_principalSubmatrix {R : Type u_1} {n : Nat} (M : Matrix R n n) (k : Nat) (hk : k ≤ n) (i j : Fin k) : (M.principalSubmatrix k hk)[i][j] = have ii := ⟨↑i, ⋯⟩; let jj := ⟨↑j, ⋯⟩; M[ii][jj]

Entry formula for the k × k principal submatrix.

@[simp]

theorem Hex.Matrix.row_principalSubmatrix {R : Type u_1} {n : Nat} (M : Matrix R n n) (k : Nat) (hk : k ≤ n) (i : Fin k) : (M.principalSubmatrix k hk).row i = Vector.ofFn fun (j : Fin k) => have ii := ⟨↑i, ⋯⟩; let jj := ⟨↑j, ⋯⟩; M[ii][jj]

Row i of the k × k principal submatrix is row i of M, restricted to the first k columns.

@[simp]

theorem Hex.Matrix.col_principalSubmatrix {R : Type u_1} {n : Nat} (M : Matrix R n n) (k : Nat) (hk : k ≤ n) (j : Fin k) : (M.principalSubmatrix k hk).col j = Vector.ofFn fun (i : Fin k) => have ii := ⟨↑i, ⋯⟩; let jj := ⟨↑j, ⋯⟩; M[ii][jj]

Column j of the k × k principal submatrix is column j of M, restricted to the first k rows.

theorem Hex.Matrix.getElem_takeRows {R : Type u_1} {n m : Nat} (M : Matrix R n m) (k : Nat) (hk : k ≤ n) (i : Fin k) (j : Fin m) : (M.takeRows k hk)[i][j] = have ii := ⟨↑i, ⋯⟩; M[ii][j]

Entry formula for the first-k-rows slice.

@[simp]

theorem Hex.Matrix.principalSubmatrix_identity {R : Type u} [OfNat R 0] [OfNat R 1] {n : Nat} (k : Nat) (hk : k ≤ n) : (Matrix.identity n).principalSubmatrix k hk = Matrix.identity k

The leading principal k × k submatrix of the identity is the identity.