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.adjugate_mul {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) : M.adjugate * M = M.det • Matrix.identity (n + 1)

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

The left-hand companion to mul_adjugate. Having both sides in matrix form is what lets a one-sided inverse be turned into a two-sided one; see mul_eq_one_comm.

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.ofFn_mem_permutationVectors {n : Nat} (cols : Fin n → Fin n) (hcols : Function.Injective cols) : Vector.ofFn cols ∈ permutationVectors n

theorem Hex.Matrix.columnTupleMatrix_eq_ofFn_ofFn {R : Type u} {n : Nat} (M : Matrix R n n) (cols : Fin n → Fin n) : M.columnTupleMatrix cols = ofFn fun (r c : Fin n) => M[r][(Vector.ofFn cols)[c]]

theorem Hex.Matrix.det_columnTupleMatrix_of_injective {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R n n) (cols : Fin n → Fin n) (hcols : Function.Injective cols) : (M.columnTupleMatrix cols).det = detSign (Vector.ofFn cols) * M.det

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 is the two-by-two difference of the four one-row cofactor-row pairings of u and v.

This is the two-by-two case of Jacobi's identity for minors of the adjugate, written with row replacement rather than row deletion. It is not the general Sylvester determinant identity, the statement that an m by m matrix of bordered minors has determinant det A0 ^ (m - 1) * det A, which is not proved in this project.

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 identity: replacing distinct rows a and b of M by u and v relates det M times the doubly-replaced determinant to the four singly-replaced determinants.

Substituting standard basis vectors for u and v turns each singly-replaced determinant into a signed one-row/one-column minor, recovering Desnanot-Jacobi for an arbitrary row pair and column pair.

theorem Hex.Matrix.mul_eq_one_comm {R : Type u} [Lean.Grind.CommRing R] {n : Nat} {U W : Matrix R n n} (h : U * W = Matrix.identity n) : W * U = Matrix.identity n

A square matrix with a right inverse over a commutative ring has that same matrix as a left inverse.

Over a field this is linear algebra. Over a general commutative ring it needs the adjugate, because the inverse is only available as adjugate M scaled by det M, and det M is a unit exactly when M is invertible. The proof applies adjugate_mul twice: once to rewrite adjugate U as det U • W, and once to recognise det U • (W * U) as det U • 1.

The intended consumer is a certificate checker that verifies a single product U * W = 1 and reads unimodularity of U off it, rather than checking both directions or computing a determinant.