English
In a DivisionCommutative Monoid G, there is a natural multiplicative equivalence MulEquiv G G whose toFun is inversion, invFun is inversion, and with map_mul' equal to mul_inv; i.e., the inverse map is a MulEquiv.
Русский
В разделимом коммутативном моноиде G имеется естественное мультивариантное эквивалентное отображение MulEquiv G G, где отображение равно инверсиям, отображение обратного равно инверсии, и сохранение умножения задано через mul_inv.
LaTeX
$$$\\mathrm{MulEquiv}.inv : G \\simeq_* G$, с toFun = Inv.inv, invFun = Inv.inv, и map_mul' = mul_inv$$$
Lean4
/-- In a `DivisionCommMonoid`, `Equiv.inv` is a `MulEquiv`. There is a variant of this
`MulEquiv.inv' G : G ≃* Gᵐᵒᵖ` for the non-commutative case. -/
@[to_additive (attr := simps apply) /-- When the `AddGroup` is commutative, `Equiv.neg` is an `AddEquiv`. -/
]
def inv (G : Type*) [DivisionCommMonoid G] : G ≃* G :=
{ Equiv.inv G with toFun := Inv.inv, invFun := Inv.inv, map_mul' := mul_inv }
