English
If A,B,D are blocks with invertible D, and fromBlocks A B 0 D is invertible, then the inverse is given by a block expression: ⅟(fromBlocks A B 0 D) equals fromBlocks (⅟A) (−(⅟A B D^{-1})) (−(D^{-1} C ⅟A)) (⅟D).
Русский
Если блоки A,B, D удовлетворяют условиям, то обратная матрица fromBlocks A B 0 D равна блочному выражению: ⅟(fromBlocks A B 0 D) = fromBlocks (⅟A) (−(⅟A B D^{-1})) (−(D^{-1} C ⅟A)) (⅟D).
LaTeX
$$$\text{invOf}_{2 2}(\mathrm{fromBlocks}(A,B,0,D)) = \mathrm{fromBlocks}(\frac{1}{A}, -\frac{1}{A} B D^{-1}, 0, D^{-1})$$$
Lean4
theorem invOf_fromBlocks_zero₂₁_eq (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α) [Invertible A]
[Invertible D] [Invertible (fromBlocks A B 0 D)] :
⅟(fromBlocks A B 0 D) = fromBlocks (⅟A) (-(⅟A * B * ⅟D)) 0 (⅟D) :=
by
letI := fromBlocksZero₂₁Invertible A B D
convert (rfl : ⅟(fromBlocks A B 0 D) = _)
