theorem Hex.Matrix.det_identity {R : Type u} [Lean.Grind.CommRing R] {n : Nat} : (Matrix.identity n).det = 1

The determinant of the identity matrix is one.

theorem Hex.Matrix.det_rowSwap {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R n n) (i j : Fin n) (h : i ≠ j) : (M.rowSwap i j).det = -M.det

Swapping two distinct rows negates the determinant.

theorem Hex.Matrix.det_rowScale {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R n n) (i : Fin n) (c : R) : (M.rowScale i c).det = c * M.det

Scaling a row by c scales the determinant by c.

theorem Hex.Matrix.det_rowAdd {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R n n) (src dst : Fin n) (c : R) (h : src ≠ dst) : (M.rowAdd src dst c).det = M.det

Adding a multiple of one row to a distinct row preserves the determinant.

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

The determinant is invariant under matrix transpose.

theorem Hex.Matrix.cofactor_transpose {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (row col : Fin (n + 1)) : M.transpose.cofactor row col = M.cofactor col row

Cofactors commute with transpose after swapping the row and column indices.

theorem Hex.Matrix.det_colPermute_vector {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R n n) (sigma : Vector (Fin n) n) (hsigma : sigma ∈ permutationVectors n) : (ofFn fun (r c : Fin n) => M[r][sigma[c]]).det = detSign sigma * M.det

Permuting columns multiplies the determinant by the sign of the column permutation.

theorem Hex.Matrix.det_colSwap {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R n n) (i j : Fin n) (h : i ≠ j) : (M.colSwap i j).det = -M.det

Swapping two distinct columns negates the determinant. The column mirror of Hex.Matrix.det_rowSwap, proved by transposing to the row law.

theorem Hex.Matrix.det_colScale {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R n n) (j : Fin n) (c : R) : (M.colScale j c).det = c * M.det

Scaling a column by c scales the determinant by c. The column mirror of det_rowScale.

theorem Hex.Matrix.det_colAdd {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R n n) (src dst : Fin n) (c : R) (h : src ≠ dst) : (M.colAdd src dst c).det = M.det

Adding a multiple of one column to a distinct column preserves determinant.