English
Analogous to the upper-triangular case: a lower-block-triangular matrix is invertible if its diagonal blocks are invertible, i.e., fromBlocks A 0 C D is invertible whenever A and D invertible.
Русский
Аналогично верхнему случаю: нижне-блочно-треугольная матрица обратима, если диагональные блоки обратимы.
LaTeX
$$$\text{Invertible}(\mathrm{fromBlocks}(A,0,C,D)) \iff \text{Invertible}(A) \land \text{Invertible}(D)$$$
Lean4
/-- A lower-block-triangular matrix is invertible if its diagonal is. -/
def fromBlocksZero₁₂Invertible (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] [Invertible D] :
Invertible (fromBlocks A 0 C D) :=
invertibleOfLeftInverse _ (fromBlocks (⅟A) 0 (-(⅟D * C * ⅟A)) (⅟D)) <| by
-- a symmetry argument is more work than just copying the proof
simp_rw [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul, zero_add, add_zero, Matrix.neg_mul, invOf_mul_self,
Matrix.invOf_mul_cancel_right, neg_add_cancel, fromBlocks_one]
