Laplaces_Expansion_Theorem_v2
Proveddeterminantlaplace-expansionlinear-algebramatrixproofwiki
Let be the determinant of order . Let be integers such that Let be an order- minor of . Let be the cofactor of . Then A similar result applies for columns.
Preamble
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Formal statement
theorem Laplaces_Expansion_Theorem_v2 {R : Type _} [CommRing R] {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) (i : Fin n.succ) : A.det = ∑ j : Fin n.succ, (-1) ^ ((i : ℕ) + (j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det := by sorrySource