theorem desnanot_jacobi {R : Type u_2} [CommRing R] {n : ℕ} (M : Matrix (Fin (n + 2)) (Fin (n + 2)) R) : M.det * (M.submatrix (Fin.succAbove 0 ∘ (Fin.last n).succAbove) (Fin.succAbove 0 ∘ (Fin.last n).succAbove)).det = (M.submatrix (Fin.succAbove 0) (Fin.succAbove 0)).det * (M.submatrix (Fin.last (n + 1)).succAbove (Fin.last (n + 1)).succAbove).det - (M.submatrix (Fin.succAbove 0) (Fin.last (n + 1)).succAbove).det * (M.submatrix (Fin.last (n + 1)).succAbove (Fin.succAbove 0)).det

The Desnanot-Jacobi identity (Lewis Carroll identity, Dodgson condensation): for any (n+2) × (n+2) matrix M over a commutative ring, det(M) · det(M_interior) = det(M₁₁) · det(Mₙₙ) - det(M₁ₙ) · det(Mₙ₁).