Determinant column linearity for hex-matrix.

This module proves that det is multilinear in a single replaced column. Working from the per-permutation product detProduct and signed term detTerm, it establishes the additive det_setCol_add, the scalar det_setCol_smul, and the finite-list/Fin m aggregated forms det_setCol_sum_list and det_setCol_sum_finRange. It also collects the duplicate-column/row vanishing lemmas (det_eq_zero_of_col_eq, det_eq_zero_of_row_eq) and det_setCol_add_otherCols (column operations preserve the determinant), plus the columnSumMatrix builder and the Fubini sum-swap List.foldl_add_comm used by the Cauchy-Binet expansion.

theorem Hex.Matrix.det_setCol_add {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R n n) (dst : Fin n) (v w : Fin n → R) : (M.setCol dst fun (r : Fin n) => v r + w r).det = (M.setCol dst v).det + (M.setCol dst w).det

Determinant linearity in one replaced column, additive form.

theorem Hex.Matrix.det_setCol_smul {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R n n) (dst : Fin n) (c : R) (v : Fin n → R) : (M.setCol dst fun (r : Fin n) => c * v r).det = c * (M.setCol dst v).det

Determinant linearity in one replaced column, scalar form.

theorem Hex.Matrix.det_setRow_add {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R n n) (dst : Fin n) (v w : Vector R n) : (M.setRow dst (Vector.ofFn fun (c : Fin n) => v[c] + w[c])).det = (M.setRow dst v).det + (M.setRow dst w).det

Determinant linearity in one replaced row, additive form. The row mirror of det_setCol_add, proved by transposing to the column law.

theorem Hex.Matrix.det_setCol_sum_list {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R n n) (dst : Fin n) {β : Type v} (xs : List β) (coeff : β → R) (source : β → Fin n → R) : (M.setCol dst fun (r : Fin n) => List.foldl (fun (acc : R) (x : β) => acc + coeff x * source x r) 0 xs).det = List.foldl (fun (acc : R) (x : β) => acc + coeff x * (M.setCol dst (source x)).det) 0 xs

Determinant linearity in one replaced column, finite-list form.

theorem Hex.Matrix.det_setCol_sum_finRange {R : Type u} [Lean.Grind.CommRing R] {n m : Nat} (M : Matrix R n n) (dst : Fin n) (coeff : Fin m → R) (source : Fin m → Fin n → R) : (M.setCol dst fun (r : Fin n) => List.foldl (fun (acc : R) (x : Fin m) => acc + coeff x * source x r) 0 (List.finRange m)).det = List.foldl (fun (acc : R) (x : Fin m) => acc + coeff x * (M.setCol dst (source x)).det) 0 (List.finRange m)

Determinant linearity in one replaced column, indexed by Fin m.

def Hex.Matrix.columnSumMatrix {R : Type u} [Lean.Grind.CommRing R] {n m : Nat} (source coeff : Matrix R n m) : Matrix R n n

Square matrix whose j-th column is the finite linear combination of the columns of source with coefficients from row j of coeff.

Equations

• source.columnSumMatrix coeff = Hex.Matrix.ofFn fun (r j : Fin n) => Fin.foldl m (fun (acc : R) (k : Fin m) => acc + coeff[(j, k)] * source[(r, k)]) 0

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

A determinant with two equal rows is zero.

theorem Hex.Matrix.det_eq_zero_of_col_eq {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R n n) (src dst : Fin n) (h : src ≠ dst) (hcol : ∀ (r : Fin n), M[r][src] = M[r][dst]) : M.det = 0

A determinant with two equal columns is zero.

theorem Hex.Matrix.det_setCol_existing_col_eq_zero {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R n n) (dst src : Fin n) (hsrcdst : src ≠ dst) : (M.setCol dst fun (r : Fin n) => M[r][src]).det = 0

Replacing a column by an already-present different column creates a duplicate column, so the determinant is zero.

theorem Hex.Matrix.det_setCol_add_otherCols {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R n n) (dst : Fin n) (sources : List (Fin n)) (coeff : Fin n → R) (hsrc : ∀ (s : Fin n), s ∈ sources → s ≠ dst) : (M.setCol dst fun (r : Fin n) => M[r][dst] + List.foldl (fun (acc : R) (s : Fin n) => acc + coeff s * M[r][s]) 0 sources).det = M.det

Adding a finite linear combination of other columns of M to column dst preserves the determinant. The sources are given as a list and each source is required to differ from dst.

All-column ordered tuple expansion

Iterates det_columnSumMatrix_expand_column over every column to express det (columnSumMatrix source coeff) as a sum over ordered column tuples. Uses a list-based "left prefix" partial assignment, with a Fubini-style sum-swap to align the iteration order with columnTupleVectors.