English
The pair of equivalences between invertibles on tsze_R M and on R forms an equivalence of types; each direction is canonically given by fst and its inverse construction.
Русский
Парное соответствие между обратимыми в tsze_R M и в R образует эквивалентность типов; каждое направление задаётся fst и строением обратного.
LaTeX
$$$ Inv(tsze_R M) \\simeq Inv(R) $$$
Lean4
/-- Together `TrivSqZeroExt.detInvertibleOfInvertible` and `TrivSqZeroExt.invertibleOfDetInvertible`
form an equivalence, although both sides of the equiv are subsingleton anyway. -/
@[simps]
def invertibleEquivInvertibleFst (x : tsze R M) : Invertible x ≃ Invertible x.fst
where
toFun _ := invertibleFstOfInvertible x
invFun _ := invertibleOfInvertibleFst x
left_inv _ := Subsingleton.elim _ _
right_inv _ := Subsingleton.elim _ _
