English
An upper-block-triangular matrix is invertible if and only if each diagonal block is invertible. In particular, fromBlocks A B 0 D is invertible whenever A and D are invertible.
Русский
Верхне-блочно-треугольная матрица обратима тогда и только тогда, когда диагональные блоки обратимы.
LaTeX
$$$\text{Invertible}(\mathrm{fromBlocks}(A,B,0,D)) \iff \text{Invertible}(A) \land \text{Invertible}(D)$$$
Lean4
/-- An upper-block-triangular matrix is invertible if its diagonal is. -/
def fromBlocksZero₂₁Invertible (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α) [Invertible A] [Invertible D] :
Invertible (fromBlocks A B 0 D) :=
invertibleOfLeftInverse _ (fromBlocks (⅟A) (-(⅟A * B * ⅟D)) 0 (⅟D)) <| by
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, add_neg_cancel, fromBlocks_one]
