English
Symmetric to the previous case: if the whole block matrix is invertible and the top-left block A is invertible, then the bottom-right Schur complement D − C A^{-1} B is invertible.
Русский
Симметрично к предыдущему случаю: если вся блочная матрица обратима и A обращима, то нижний правый Шур-комплемент D − C A^{-1} B обратим.
LaTeX
$$$\text{Invertible}(\mathrm{fromBlocks}(A,B,C,D)) \Rightarrow \text{Invertible}(D - C A^{-1} B)$$$
Lean4
/-- If a block matrix is invertible and so is its bottom left element, then so is the corresponding
Schur complement. -/
def invertibleOfFromBlocks₁₁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) := by
-- another symmetry argument
letI iABCD' := submatrixEquivInvertible (fromBlocks A B C D) (Equiv.sumComm _ _) (Equiv.sumComm _ _)
letI iDCBA := iABCD'.copy _ (fromBlocks_submatrix_sum_swap_sum_swap _ _ _ _).symm
exact invertibleOfFromBlocks₂₂Invertible D C B A
