The Desnanot-Jacobi identity #
We prove the Desnanot-Jacobi identity (also known as the Lewis Carroll identity
or Dodgson condensation identity): for any matrix M over a commutative ring,
det(M) * det(M₁ₖ¹ᵏ) = det(M₁¹) * det(Mₖᵏ) - det(M₁ᵏ) * det(Mₖ¹),
where subscripts and superscripts denote row and column deletion.
The proof proceeds by multiplying M by an auxiliary matrix built from the adjugate.
Main results #
desnanot_jacobi: the Desnanot-Jacobi identity over any commutative ring.
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ₙ₁).