English
Assume D is invertible. The matrix fromBlocks(A,B,C,D) is a unit (has a multiplicative inverse in the matrix ring) if and only if the Schur complement A − B D^{-1} C is a unit.
Русский
Пусть D обратима. Тогда матрица fromBlocks(A,B,C,D) является единицей (имеет обратную) тогда и только тогда, когда Schur-комплемент A − B D^{-1} C является единицей.
LaTeX
$$$\\operatorname{IsUnit}(\\mathrm{fromBlocks}(A,B,C,D)) \\iff \\operatorname{IsUnit}(A - B D^{-1} C) \\text{ (with } [\\operatorname{Invertible} D]\\text{)}$$$
Lean4
/-- If the bottom-left element of a block matrix is invertible, then the whole matrix is invertible
iff the corresponding Schur complement is. -/
theorem isUnit_fromBlocks_iff_of_invertible₂₂ {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α}
{D : Matrix n n α} [Invertible D] : IsUnit (fromBlocks A B C D) ↔ IsUnit (A - B * ⅟D * C) := by
simp only [← nonempty_invertible_iff_isUnit, (invertibleEquivFromBlocks₂₂Invertible A B C D).nonempty_congr]
