English
If the bottom-right block D is invertible, the determinant of the block matrix fromBlocks(A,B,C,D) equals det(D) times det(A − B D^{-1} C).
Русский
Если правый нижний блок D обратим, детерминант fromBlocks(A,B,C,D) равен det(D) умножить на det(A − B D^{-1} C).
LaTeX
$$$\\det\\mathrm{fromBlocks}(A,B,C,D) = \\det(D) \\cdot \\det\\bigl(A - B D^{-1} C\\bigr) \\quad (D \\text{ invertible})$$$
Lean4
/-- Determinant of a 2×2 block matrix, expanded around an invertible bottom right element in terms
of the Schur complement. -/
theorem det_fromBlocks₂₂ (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible D] :
(Matrix.fromBlocks A B C D).det = det D * det (A - B * ⅟D * C) :=
by
have : fromBlocks A B C D = (fromBlocks D C B A).submatrix (Equiv.sumComm _ _) (Equiv.sumComm _ _) :=
by
ext (i j)
cases i <;> cases j <;> rfl
rw [this, det_submatrix_equiv_self, det_fromBlocks₁₁]
