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.