theorem Hex.Matrix.deleteRowCol_setRow_self {R : Type u} {n : Nat} (M : Matrix R (n + 1) (n + 1)) (dst col : Fin (n + 1)) (v : Vector R (n + 1)) : (M.setRow dst v).deleteRowCol dst col = M.deleteRowCol dst col

Deleting the destination row of setRow M dst v gives the same minor as deleting the destination row of M: the replaced row is removed anyway, so the new entries are invisible.

theorem Hex.Matrix.cofactor_setRow_self {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (dst col : Fin (n + 1)) (v : Vector R (n + 1)) : (M.setRow dst v).cofactor dst col = M.cofactor dst col

The cofactor expansion of setRow M dst v along the replaced row dst uses the same minors as the cofactor expansion of M along that row, because the deleted row never contributes to the minor.

def Hex.Matrix.cofactorRowPairing {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (row : Fin (n + 1)) (v : Vector R (n + 1)) : R

Pair a row vector with a cofactor row of M. This is the scalar that appears in Laplace expansion after replacing the expanded row.

Equations

• M.cofactorRowPairing row v = Fin.foldl (n + 1) (fun (acc : R) (col : Fin (n + 1)) => acc + v[col] * M.cofactor row col) 0

theorem Hex.Matrix.det_setRow_eq_cofactorRowPairing {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (row : Fin (n + 1)) (v : Vector R (n + 1)) : (M.setRow row v).det = M.cofactorRowPairing row v

Replacing row row by v makes the determinant the pairing of v against the original cofactor row.

theorem Hex.Matrix.cofactorRowPairing_self {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (row : Fin (n + 1)) : M.cofactorRowPairing row M[row] = M.det

Pairing the original row against its own cofactor row recovers det M.

theorem Hex.Matrix.foldl_alien_cofactor_eq_zero {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (i j : Fin (n + 1)) (hij : i ≠ j) : Fin.foldl (n + 1) (fun (acc : R) (k : Fin (n + 1)) => acc + M[i][k] * M.cofactor j k) 0 = 0

The "alien cofactor" identity: expanding row i of M against the cofactors of a different row j produces zero. This is the characteristic vanishing identity that makes the adjugate work.

theorem Hex.Matrix.cofactorRowPairing_alien_eq_zero {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (i j : Fin (n + 1)) (hij : i ≠ j) : M.cofactorRowPairing j M[i] = 0

Pairing an unreplaced row of M against a different cofactor row is zero.

def Hex.Matrix.adjugate {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) : Matrix R (n + 1) (n + 1)

The local adjugate matrix: entry (i, j) is the cofactor at row j, column i of M. This is the transpose of the cofactor matrix.

Equations

• M.adjugate = Hex.Matrix.ofFn fun (i j : Fin (n + 1)) => M.cofactor j i

theorem Hex.Matrix.adjugate_get {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (i j : Fin (n + 1)) : M.adjugate[i][j] = M.cofactor j i

Entry (i, j) of the adjugate is the cofactor of M at row j, column i (the transpose of the cofactor matrix).

theorem Hex.Matrix.mul_adjugate_apply {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (i j : Fin (n + 1)) : (M * M.adjugate)[i][j] = if i = j then M.det else 0

Entrywise version of M * adjugate M = det M • 1. On the diagonal this is Laplace expansion of det M; off the diagonal it is the alien cofactor identity.

theorem Hex.Matrix.mul_adjugate {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) : M * M.adjugate = M.det • Matrix.identity (n + 1)

The adjugate identity M * adjugate M = det M • identity.

theorem Hex.Matrix.adjugate_mul_apply {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (i j : Fin (n + 1)) : (M.adjugate * M)[i][j] = if i = j then M.det else 0

Entrywise version of adjugate M * M = det M • 1.

This is the transpose-side companion to mul_adjugate_apply; it is useful when cofactor identities are consumed columnwise rather than rowwise.

theorem Hex.Matrix.mul_adjugate_apply_zero {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (i : Fin (n + 1)) : (M * M.adjugate)[i][0] = if i = 0 then M.det else 0

Column-0 view of M * adjugate M.

theorem Hex.Matrix.mul_adjugate_apply_last {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (i : Fin (n + 1)) : (M * M.adjugate)[i][Fin.last n] = if i = Fin.last n then M.det else 0

Last-column view of M * adjugate M.

theorem Hex.Matrix.adjugate_eq_cofactorSign_mul_deleteRowCol {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (i j : Fin (n + 1)) : M.adjugate[i][j] = cofactorSign j i * (M.deleteRowCol j i).det

Cofactor-minor representation of an adjugate entry.

theorem Hex.Matrix.adjugate_zero_zero {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) : M.adjugate[0][0] = (M.deleteRowCol 0 0).det

The (0, 0) adjugate entry equals the determinant of the minor obtained by deleting row 0 and column 0.

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

The (Fin.last, Fin.last) adjugate entry equals the determinant of the leading prefix minor obtained by deleting the last row and column.

theorem Hex.Matrix.det_mul {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M N : Matrix R n n) : (M * N).det = M.det * N.det

Determinant of a product of square matrices.

This is the Mathlib-free Cauchy-Binet specialization already used by the Desnanot-Jacobi auxiliary proof.

theorem Hex.Matrix.cofactorRowPairing_setRow_plucker {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (a b : Fin (n + 1)) (hab : a ≠ b) (u v : Vector R (n + 1)) : M.det * (M.setRow a u).cofactorRowPairing b v = M.cofactorRowPairing a u * M.cofactorRowPairing b v - M.cofactorRowPairing a v * M.cofactorRowPairing b u

Two-row replacement determinant Plucker kernel.

For matrix M : Matrix R (n+1) (n+1), distinct rows a and b, and replacement vectors u, v, the determinant of M paired with the two-row-replaced cofactor-row pairing satisfies the quadratic Sylvester relation against the four one-row cofactor-row pairings of u and v.

theorem Hex.Matrix.det_setRow_setRow_mul_det {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (a b : Fin (n + 1)) (hab : a ≠ b) (u v : Vector R (n + 1)) : M.det * ((M.setRow a u).setRow b v).det = (M.setRow a u).det * (M.setRow b v).det - (M.setRow a v).det * (M.setRow b u).det

Two-row replacement determinant Plucker identity.