English
Symmetric to the₂₂ case: if A and D are invertible and fromBlocks A 0 C D is invertible, then its inverse is given by a block expression: ⅟(fromBlocks A 0 C D) = fromBlocks (⅟A) 0 (−(D^{-1} C ⁻¹ A⁻¹)) D⁻¹.
Русский
Симметрично к предыдущему случае: если A и D обратимы и fromBlocks A 0 C D обратима, то её обратная имеет блочное представление.
LaTeX
$$$[\text{Invertible}(A) \land \text{Invertible}(D)] \Rightarrow \ ⅟(\mathrm{fromBlocks}(A,0,C,D)) = \mathrm{fromBlocks}(A^{-1}, 0, -(D^{-1} C A^{-1}), D^{-1})$$$
Lean4
theorem invOf_fromBlocks_zero₁₂_eq (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A]
[Invertible D] [Invertible (fromBlocks A 0 C D)] :
⅟(fromBlocks A 0 C D) = fromBlocks (⅟A) 0 (-(⅟D * C * ⅟A)) (⅟D) :=
by
letI := fromBlocksZero₁₂Invertible A C D
convert (rfl : ⅟(fromBlocks A 0 C D) = _)
