English
An equivalence between the invertibility of A.submatrix e1 e2 and the invertibility of A is established by submatrixEquivInvertible and invertibleOfSubmatrixEquivInvertible.
Русский
Эквивалентность между обратимостью A.submatrix e1 e2 и обратимостью A устанавливается через submatrixEquivInvertible и invertibleOfSubmatrixEquivInvertible.
LaTeX
$$Invertible(A.submatrix e1 e2) ≃ Invertible A$$
Lean4
/-- Together `Matrix.submatrixEquivInvertible` and
`Matrix.invertibleOfSubmatrixEquivInvertible` form an equivalence, although both sides of the
equiv are subsingleton anyway. -/
@[simps]
def submatrixEquivInvertibleEquivInvertible (A : Matrix m m α) (e₁ e₂ : n ≃ m) :
Invertible (A.submatrix e₁ e₂) ≃ Invertible A
where
toFun _ := invertibleOfSubmatrixEquivInvertible A e₁ e₂
invFun _ := submatrixEquivInvertible A e₁ e₂
left_inv _ := Subsingleton.elim _ _
right_inv _ := Subsingleton.elim _ _
