English
Invertibility of a block matrix fromBlocks is equivalent to invertibility of its diagonal blocks; i.e., is invertible iff both diagonal blocks are invertible.
Русский
Обратимость fromBlocks эквивалентна обратимости диагональных блоков: обратима тогда и только тогда, когда оба диагональных блока обращимы.
LaTeX
$$$\text{IsUnit}(\mathrm{fromBlocks}(A,0,C,D)) \iff (\text{IsUnit}(A) \land \text{IsUnit}(D))$$$
Lean4
/-- A lower block-triangular matrix is invertible iff both elements of its diagonal are.
This is a propositional form of `Matrix.fromBlocksZero₁₂InvertibleEquiv` forms an `iff`. -/
@[simp]
theorem isUnit_fromBlocks_zero₁₂ {A : Matrix m m α} {C : Matrix n m α} {D : Matrix n n α} :
IsUnit (fromBlocks A 0 C D) ↔ IsUnit A ∧ IsUnit D := by
simp only [← nonempty_invertible_iff_isUnit, ← nonempty_prod, (fromBlocksZero₁₂InvertibleEquiv _ _ _).nonempty_congr]
