English
For invertible D and A,B,C, the inverse of fromBlocks A B C D is given by a block expression in terms of A, B, C, D and their inverses, when fromBlocks A B 0 D is invertible.
Русский
Для обратимых D и A,B,C обратная матрица fromBlocks A B C D выражается через инверторы блочных частей.
LaTeX
$$$\bigl\{ \text{Invertible}(A), \text{Invertible}(D) \bigr\} \Rightarrow ⅟(\mathrm{fromBlocks}(A,B,C,D)) = \mathrm{fromBlocks}(\mathrm{inv}(A), -\mathrm{inv}(A) B D^{-1}, -D^{-1} C \mathrm{inv}(A), D^{-1})$$$
Lean4
theorem invOf_fromBlocks₂₂_eq (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible D]
[Invertible (A - B * ⅟D * C)] [Invertible (fromBlocks A B C D)] :
⅟(fromBlocks A B C D) =
fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * B * ⅟D)) (-(⅟D * C * ⅟(A - B * ⅟D * C)))
(⅟D + ⅟D * C * ⅟(A - B * ⅟D * C) * B * ⅟D) :=
by
letI := fromBlocks₂₂Invertible A B C D
convert (rfl : ⅟(fromBlocks A B C D) = _)
