English
Assume A is invertible. The determinant of the block matrix fromBlocks(A,B,C,D) factors as det A times the determinant of the Schur complement D − C A^{-1} B.
Русский
Пусть A обратима. Определитель блочной матрицы fromBlocks(A,B,C,D) распадается как det A умножить на det(D − C A^{-1} B).
LaTeX
$$$\\det\\mathrm{fromBlocks}(A,B,C,D) = \\det(A) \\cdot \\det\\bigl(D - C A^{-1} B\\bigr) \\quad (A \\text{ invertible})$$$
Lean4
/-- Determinant of a 2×2 block matrix, expanded around an invertible top left 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 A] :
(Matrix.fromBlocks A B C D).det = det A * det (D - C * ⅟A * B) := by
rw [fromBlocks_eq_of_invertible₁₁ (A := A), det_mul, det_mul, det_fromBlocks_zero₂₁, det_fromBlocks_zero₂₁,
det_fromBlocks_zero₁₂, det_one, det_one, one_mul, one_mul, mul_one]
