English
If A is invertible, then the invertibility of the block matrix fromBlocks(A,B,C,D) is equivalent to the invertibility of the Schur complement D − C A^{-1} B.
Русский
Если A обратима, то обратимость блочной матрицы fromBlocks(A,B,C,D) эквивалентна обратимости Schur-комплементa D − C A^{-1} B.
LaTeX
$$$\\operatorname{Invertible}(\\mathrm{fromBlocks}(A,B,C,D)) \\simeq \\operatorname{Invertible}(D - C A^{-1} B)\\quad (A \\text{ invertible})$$$
Lean4
/-- If the top-right 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 A] : IsUnit (fromBlocks A B C D) ↔ IsUnit (D - C * ⅟A * B) := by
simp only [← nonempty_invertible_iff_isUnit, (invertibleEquivFromBlocks₁₁Invertible A B C D).nonempty_congr]
