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.