English
There is an equivalence between invertibility of fromBlocks A 0 C D and the pair (Invertible A, Invertible D).
Русский
Существует эквивалентность между обратимостью fromBlocks A 0 C D и парой (Invertible A, Invertible D).
LaTeX
$$$\mathrm{fromBlocksZero₁₂InvertibleEquiv}(A,C,D) : \mathrm{Invertible}(\mathrm{fromBlocks}(A,0,C,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 α) (C : Matrix n m α) (D : Matrix n n α) :
Invertible (fromBlocks A 0 C D) ≃ Invertible A × Invertible D
where
toFun _ := invertibleOfFromBlocksZero₁₂Invertible A C D
invFun
i := by
letI := i.1
letI := i.2
exact fromBlocksZero₁₂Invertible A C D
left_inv _ := Subsingleton.elim _ _
right_inv _ := Subsingleton.elim _ _
