Minors, deleted row/column submatrices, and signed cofactors.

This module defines skipIndex, the embedding of Fin n into Fin (n + 1) that skips a deleted index, and uses it to build deleteRowCol, the (n + 1) × (n + 1) minor obtained by removing one row and one column. It then introduces the alternating cofactorSign and the signed cofactor, with the simp/grind characterizations of their values by parity. Key normalizations include deleteRowCol_last_last and cofactor_last_last (bottom-right minor is the leading prefix) and deleteRowCol_transpose, the transpose-compatibility used by row/column cofactor expansion.

def Hex.Matrix.skipIndex {n : Nat} (skip : Fin (n + 1)) (i : Fin n) : Fin (n + 1)

Embed Fin n into Fin (n + 1) while skipping one deleted index.

Equations

• Hex.Matrix.skipIndex skip i = if h : ↑i < ↑skip then ⟨↑i, ⋯⟩ else ⟨↑i + 1, ⋯⟩

@[simp]

theorem Hex.Matrix.skipIndex_val_of_lt {n : Nat} (skip : Fin (n + 1)) (i : Fin n) (h : ↑i < ↑skip) : ↑(skipIndex skip i) = ↑i

The skipped-index embedding leaves entries below the deleted index unchanged. This is the low-side simp branch for row and column deletion.

@[simp]

theorem Hex.Matrix.skipIndex_val_of_not_lt {n : Nat} (skip : Fin (n + 1)) (i : Fin n) (h : ¬↑i < ↑skip) : ↑(skipIndex skip i) = ↑i + 1

The skipped-index embedding shifts entries at or above the deleted index by one. This is the high-side simp branch for row and column deletion.

theorem Hex.Matrix.skipIndex_ne {n : Nat} (skip : Fin (n + 1)) (i : Fin n) : skipIndex skip i ≠ skip

The index produced by skipIndex skip is never the deleted index skip. This is the basic side condition for minors that remove a row or column.

@[simp]

theorem Hex.Matrix.skipIndex_last {n : Nat} (i : Fin n) : skipIndex (Fin.last n) i = i.castSucc

Skipping the final index embeds Fin n by castSucc. This normalizes bottom-right minors to leading prefixes.

def Hex.Matrix.deleteRowCol {R : Type u} {n : Nat} (M : Matrix R (n + 1) (n + 1)) (row col : Fin (n + 1)) : Matrix R n n

Delete one row and one column from an (n + 1) × (n + 1) matrix.

Equations

• M.deleteRowCol row col = Hex.Matrix.ofFn fun (i j : Fin n) => M[(Hex.Matrix.skipIndex row i, Hex.Matrix.skipIndex col j)]

theorem Hex.Matrix.getElem_deleteRowCol {R : Type u} {n : Nat} (M : Matrix R (n + 1) (n + 1)) (row col : Fin (n + 1)) (i j : Fin n) : (M.deleteRowCol row col)[i][j] = M[skipIndex row i][skipIndex col j]

Entries of a deleted-row/deleted-column minor are the corresponding source entries at the skipped row and column indices.

@[simp]

theorem Hex.Matrix.deleteRowCol_last_last {R : Type u} {n : Nat} (M : Matrix R (n + 1) (n + 1)) : M.deleteRowCol (Fin.last n) (Fin.last n) = M.principalSubmatrix n ⋯

Deleting the final row and final column gives the leading prefix. This is the minor normalization used by bottom-right cofactor expansion.

theorem Hex.Matrix.deleteRowCol_transpose {R : Type u} {n : Nat} (M : Matrix R (n + 1) (n + 1)) (row col : Fin (n + 1)) : M.transpose.deleteRowCol row col = (M.deleteRowCol col row).transpose

Deleting row row and column col after transposing is the transpose of the minor obtained by deleting row col and column row before transposing.

def Hex.Matrix.cofactorSign {R : Type u} [OfNat R 1] [Neg R] {n : Nat} (row col : Fin (n + 1)) : R

The alternating sign used in signed cofactors.

Equations

• Hex.Matrix.cofactorSign row col = if (↑row + ↑col) % 2 = 0 then 1 else -1

@[simp]

theorem Hex.Matrix.cofactorSign_of_even {R : Type u} [OfNat R 1] [Neg R] {n : Nat} (row col : Fin (n + 1)) (h : (↑row + ↑col) % 2 = 0) : cofactorSign row col = 1

An even row-plus-column parity gives cofactor sign 1. This is the positive simp branch for signed cofactors.

@[simp]

theorem Hex.Matrix.cofactorSign_of_odd {R : Type u} [OfNat R 1] [Neg R] {n : Nat} (row col : Fin (n + 1)) (h : (↑row + ↑col) % 2 ≠ 0) : cofactorSign row col = -1

An odd row-plus-column parity gives cofactor sign -1. This is the negative simp branch for signed cofactors.

def Hex.Matrix.cofactor {R : Type u} [Lean.Grind.Ring R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (row col : Fin (n + 1)) : R

The signed cofactor for the local Leibniz determinant.

Equations

• M.cofactor row col = Hex.Matrix.cofactorSign row col * (M.deleteRowCol row col).det

@[simp]

theorem Hex.Matrix.cofactor_of_even {R : Type u} [Lean.Grind.Ring R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (row col : Fin (n + 1)) (h : (↑row + ↑col) % 2 = 0) : M.cofactor row col = (M.deleteRowCol row col).det

At even parity, a signed cofactor is just the determinant of its minor. This removes the sign in cofactor-expansion normalization.

@[simp]

theorem Hex.Matrix.cofactor_of_odd {R : Type u} [Lean.Grind.Ring R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (row col : Fin (n + 1)) (h : (↑row + ↑col) % 2 ≠ 0) : M.cofactor row col = -(M.deleteRowCol row col).det

At odd parity, a signed cofactor is the negated determinant of its minor. This supplies the alternating sign in cofactor-expansion normalization.

@[simp]

theorem Hex.Matrix.cofactor_last_last {R : Type u} [Lean.Grind.Ring R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) : M.cofactor (Fin.last n) (Fin.last n) = (M.principalSubmatrix n ⋯).det

The bottom-right cofactor reduces to the determinant of the leading prefix. This combines the final-index minor with its even sign.