English
If the bottom-right block D is invertible and the corresponding Schur complement A − B D^{-1} C is invertible, then the block matrix fromBlocks A B C D is invertible. Moreover, an explicit inverse is given by the stated block formula.
Русский
Если блок D внизу справа обратим и соответствующий Шур-комплемент A − B D^{-1} C обратим, то матрица fromBlocks A B C D обратима, и её обратная матрица задаётся явной формулой.
LaTeX
$$$[\text{Invertible}(D) \land \text{Invertible}(A - B D^{-1} C)] \Rightarrow \text{Invertible}(\mathrm{fromBlocks}(A,B,C,D))$$
Lean4
/-- An upper block-triangular matrix is invertible iff both elements of its diagonal are.
This is a propositional form of `Matrix.fromBlocksZero₂₁InvertibleEquiv`. -/
@[simp]
theorem isUnit_fromBlocks_zero₂₁ {A : Matrix m m α} {B : Matrix m n α} {D : Matrix n n α} :
IsUnit (fromBlocks A B 0 D) ↔ IsUnit A ∧ IsUnit D := by
simp only [← nonempty_invertible_iff_isUnit, ← nonempty_prod, (fromBlocksZero₂₁InvertibleEquiv _ _ _).nonempty_congr]
