Laplace (cofactor) expansion of the determinant.

This module proves that det expands as a signed sum of M[·][·] * cofactor along any fixed row or column. det_eq_foldl_laplace_last and det_eq_foldl_laplace_last_row handle the final column and final row, and det_eq_finFoldl_laplace_col / det_eq_finFoldl_laplace_row generalize to an arbitrary column or row, stated as a core Fin.foldl over the indices; the det_eq_foldl_laplace_col / det_eq_foldl_laplace_row reference forms state the same expansions as a List.foldl over List.finRange, bridged by Fin.foldl_eq_finRange_foldl. The general case is reduced to the last-column case by the column-move permutation moveColumnToLastValues, whose sign (-1) ^ (n - col.val) is computed via the inversion-count machinery and cancelled against the cofactor sign through cofactorSign_col_eq.

theorem Hex.Matrix.det_eq_foldl_laplace_last {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) : M.det = List.foldl (fun (acc : R) (row : Fin (n + 1)) => acc + M[row][Fin.last n] * M.cofactor row (Fin.last n)) 0 (List.finRange (n + 1))

Laplace expansion of the determinant along the final column.

theorem Hex.Matrix.det_eq_foldl_laplace_last_row {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) : M.det = List.foldl (fun (acc : R) (col : Fin (n + 1)) => acc + M[Fin.last n][col] * M.cofactor (Fin.last n) col) 0 (List.finRange (n + 1))

Laplace expansion of the determinant along the final row.

theorem Hex.Matrix.det_eq_finFoldl_laplace_col {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (col : Fin (n + 1)) : M.det = Fin.foldl (n + 1) (fun (acc : R) (row : Fin (n + 1)) => acc + M[row][col] * M.cofactor row col) 0

Laplace expansion of the determinant along an arbitrary fixed column.

theorem Hex.Matrix.det_eq_foldl_laplace_col {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (col : Fin (n + 1)) : M.det = List.foldl (fun (acc : R) (row : Fin (n + 1)) => acc + M[row][col] * M.cofactor row col) 0 (List.finRange (n + 1))

Laplace expansion along a fixed column as a List.foldl over the row indices in List.finRange; the reference form of det_eq_finFoldl_laplace_col, bridged by Fin.foldl_eq_finRange_foldl.

theorem Hex.Matrix.det_eq_finFoldl_laplace_row {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (row : Fin (n + 1)) : M.det = Fin.foldl (n + 1) (fun (acc : R) (col : Fin (n + 1)) => acc + M[row][col] * M.cofactor row col) 0

Laplace expansion of the determinant along an arbitrary fixed row, as a Fin.foldl over the column indices.

theorem Hex.Matrix.det_eq_foldl_laplace_row {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (row : Fin (n + 1)) : M.det = List.foldl (fun (acc : R) (col : Fin (n + 1)) => acc + M[row][col] * M.cofactor row col) 0 (List.finRange (n + 1))

Laplace expansion along a fixed row as a List.foldl over the column indices in List.finRange; the reference form of det_eq_finFoldl_laplace_row, bridged by Fin.foldl_eq_finRange_foldl.