transposeInvertibleEquivInvertible

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 _ _

Похожие утверждения