English
There is a natural multiplicative equivalence between a group G and its opposite given by inversion, and when G is commutative there is a distinguished MulEquiv.inv.
Русский
Существует естественная мультипликативная эквивалентность между группой G и её противоположной структурой, заданная обращением; для коммутативной группы существует особая MulEquiv.inv.
LaTeX
$$$\text{inv'}: G \to^* G^{\mathrm{op}} \text{ is a multiplicative equivalence (and when } G\text{ is commutative } \text{there is } \text{MulEquiv.inv}$)$$
Lean4
/-- Inversion on a group is a `MulEquiv` to the opposite group. When `G` is commutative, there is
`MulEquiv.inv`. -/
@[to_additive (attr := simps! -fullyApplied +simpRhs) /--
Negation on an additive group is an `AddEquiv` to the opposite group. When `G`
is commutative, there is `AddEquiv.inv`. -/
]
def inv' (G : Type*) [DivisionMonoid G] : G ≃* Gᵐᵒᵖ :=
{ (Equiv.inv G).trans opEquiv with map_mul' x y := unop_injective <| mul_inv_rev x y }
