invertibleEquivDetInvertible — Mathlib

English

The invertible equivalence is defined by exchanging A with its determinant invertibility and vice versa.

Русский

Определение эквивалентности обратимости между A и det(A) через соответствующие преобразования.

LaTeX

$$def invertibleEquivDetInvertible : Invertible A ≃ Invertible A.det$$

Lean4

/-- Together `Matrix.detInvertibleOfInvertible` and `Matrix.invertibleOfDetInvertible` form an
equivalence, although both sides of the equiv are subsingleton anyway. -/
@[simps]
def invertibleEquivDetInvertible : Invertible A ≃ Invertible A.det
    where
  toFun := @detInvertibleOfInvertible _ _ _ _ _ A
  invFun := @invertibleOfDetInvertible _ _ _ _ _ A
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _

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