English
Let A, B, C, D be as above, but now A is assumed invertible. The block matrix fromBlocks(A,B,C,D) is invertible if and only if the Schur complement D − C A^{-1} B is invertible, and these invertibilities are in bijection.
Русский
Пусть A, B, C, D как выше, но теперь A обратима. Тогда fromBlocks(A,B,C,D) обратима тогда и только тогда, когда D − C A^{-1} B обратим, и эти свойства взаимно соответствуют.
LaTeX
$$$\\operatorname{Invertible}(\\mathrm{fromBlocks}(A,B,C,D)) \\simeq\\operatorname{Invertible}(D - C A^{-1} B) \\, (A \\text{ invertible})$$$
Lean4
/-- `Matrix.invertibleOfFromBlocks₁₁Invertible` and `Matrix.fromBlocks₁₁Invertible` as an
equivalence. -/
def invertibleEquivFromBlocks₁₁Invertible (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α)
[Invertible A] : Invertible (fromBlocks A B C D) ≃ Invertible (D - C * ⅟A * B)
where
toFun _iABCD := invertibleOfFromBlocks₁₁Invertible _ _ _ _
invFun _i_schur := fromBlocks₁₁Invertible _ _ _ _
left_inv _iABCD := Subsingleton.elim _ _
right_inv _i_schur := Subsingleton.elim _ _
