English
There is an equivalence between invertibility of the whole block matrix and the pair of invertibilities (A inverse, D inverse) in the ₂₁ arrangement.
Русский
Существует эквивалентность между обратимостью всей блочной матрицы и парой обратимостей (A, D) в конфигурации ₂₁.
LaTeX
$$$\mathrm{fromBlocksZero₂₁InvertibleEquiv}(A,B,D) : \mathrm{Invertible}(\mathrm{fromBlocks}(A,B,0,D)) \simeq \mathrm{Invertible}(A) \times \mathrm{Invertible}(D)$$$
Lean4
/-- `invertibleOfFromBlocksZero₂₁Invertible` and `Matrix.fromBlocksZero₂₁Invertible` form
an equivalence. -/
def fromBlocksZero₂₁InvertibleEquiv (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α) :
Invertible (fromBlocks A B 0 D) ≃ Invertible A × Invertible D
where
toFun _ := invertibleOfFromBlocksZero₂₁Invertible A B D
invFun
i := by
letI := i.1
letI := i.2
exact fromBlocksZero₂₁Invertible A B D
left_inv _ := Subsingleton.elim _ _
right_inv _ := Subsingleton.elim _ _
