English
There is an equivalence between invertible matrices and invertible transposes: Invertible(A^T) ≃ Invertible(A).
Русский
Существует эквивалентность между обратимыми матрицами и обратимыми транспонированными матрицами: Invertible(A^T) ≃ Invertible(A).
LaTeX
$$$\text{Invertible}(A^{T}) \simeq \text{Invertible}(A)$$$
Lean4
/-- Together `Matrix.invertibleTranspose` and `Matrix.invertibleOfInvertibleTranspose` form an
equivalence, although both sides of the equiv are subsingleton anyway. -/
@[simps]
def transposeInvertibleEquivInvertible : Invertible Aᵀ ≃ Invertible A
where
toFun := @invertibleOfInvertibleTranspose _ _ _ _ _ _
invFun := @invertibleTranspose _ _ _ _ _ _
left_inv _ := Subsingleton.elim _ _
right_inv _ := Subsingleton.elim _ _