English
The type RingInvo R carries an EquivLike structure with respect to R and its opposite, i.e., RingInvo R is canonically equivalent to R via its underlying map and its inverse given by the involution.
Русский
У типа RingInvo R имеется структура EquivLike относительно R и Rᵐᵒᵖ, то есть RingInvo R канонически эквивалентно R через соответствующее отображение и его обратное, заданное инволюцией.
LaTeX
$$$\text{RingInvo}(R) \;\equiv\; R \quad\text{via the underlying equivalence given by the involution.}$$$
Lean4
instance : EquivLike (RingInvo R) R Rᵐᵒᵖ where
coe f := f.toFun
inv f := f.invFun
coe_injective' e f h₁
h₂ := by
rcases e with ⟨⟨tE, _⟩, _⟩; rcases f with ⟨⟨tF, _⟩, _⟩
cases tE
cases tF
congr
left_inv f := f.left_inv
right_inv f := f.right_inv
