Bordered leading minors used by Bareiss-style determinant arguments.

def Hex.Matrix.borderedMinor {R : Type u_1} {n : Nat} (M : Matrix R n n) (k : Nat) (hk : k < n) (i j : Fin n) : Matrix R (k + 1) (k + 1)

Bordered Bareiss minor with the first k rows/columns and one extra border row i and column j. For Bareiss applications i and j are in the trailing part, but the constructor is total and leaves that side condition to the invariant using it.

Equations

• M.borderedMinor k hk i j = Hex.Matrix.ofFn fun (r c : Fin (k + 1)) => have rr := if hr : ↑r < k then ⟨↑r, ⋯⟩ else i; have cc := if hc : ↑c < k then ⟨↑c, ⋯⟩ else j; M[(rr, cc)]

theorem Hex.Matrix.borderedMinor_entry_lt_lt {R : Type u_1} {n : Nat} (M : Matrix R n n) (k : Nat) (hk : k < n) (i j : Fin n) (r c : Fin (k + 1)) (hr : ↑r < k) (hc : ↑c < k) : (M.borderedMinor k hk i j)[r][c] = have rr := ⟨↑r, ⋯⟩; have cc := ⟨↑c, ⋯⟩; M[(rr, cc)]

Interior-block case of the bordered-minor entry formula.

theorem Hex.Matrix.borderedMinor_entry_lt_last {R : Type u_1} {n : Nat} (M : Matrix R n n) (k : Nat) (hk : k < n) (i j : Fin n) (r : Fin (k + 1)) (hr : ↑r < k) : (M.borderedMinor k hk i j)[r][Fin.last k] = have rr := ⟨↑r, ⋯⟩; M[rr][j]

Border-column case of the bordered-minor entry formula.

theorem Hex.Matrix.borderedMinor_entry_last_lt {R : Type u_1} {n : Nat} (M : Matrix R n n) (k : Nat) (hk : k < n) (i j : Fin n) (c : Fin (k + 1)) (hc : ↑c < k) : (M.borderedMinor k hk i j)[Fin.last k][c] = let cc := ⟨↑c, ⋯⟩; M[i][cc]

Border-row case of the bordered-minor entry formula.

theorem Hex.Matrix.borderedMinor_entry_last_last {R : Type u_1} {n : Nat} (M : Matrix R n n) (k : Nat) (hk : k < n) (i j : Fin n) : (M.borderedMinor k hk i j)[Fin.last k][Fin.last k] = M[i][j]

Corner case of the bordered-minor entry formula.

theorem Hex.Matrix.principalSubmatrix_borderedMinor_eq_principalSubmatrix {R : Type u_1} {n : Nat} (M : Matrix R n n) (k : Nat) (hk : k < n) (i j : Fin n) : (M.borderedMinor k hk i j).principalSubmatrix k ⋯ = M.principalSubmatrix k ⋯

The top-left k × k block of a bordered minor is the leading prefix of the source matrix.

theorem Hex.Matrix.principalSubmatrix_borderedMinor_succ_eq_borderedMinor {R : Type u_1} {n : Nat} (M : Matrix R n n) (k : Nat) (hk : k < n) (hnext : k + 1 < n) (i j : Fin n) : (M.borderedMinor (k + 1) hnext i j).principalSubmatrix (k + 1) ⋯ = M.borderedMinor k hk ⟨k, hk⟩ ⟨k, hk⟩

The top-left (k + 1) × (k + 1) block of the next bordered minor is the current bordered minor whose extra row/column are the k-th source row/column.