Lean4
/-- Given a pair of monoid homomorphisms `f`, `g` such that `g.comp f = id` and `f.comp g = id`,
returns a multiplicative equivalence with `toFun = f` and `invFun = g`. This constructor is
useful if the underlying type(s) have specialized `ext` lemmas for monoid homomorphisms. -/
@[to_additive (attr := simps -fullyApplied) /--
Given a pair of additive monoid homomorphisms `f`, `g` such that `g.comp f = id`
and `f.comp g = id`, returns an additive equivalence with `toFun = f` and `invFun = g`. This
constructor is useful if the underlying type(s) have specialized `ext` lemmas for additive
monoid homomorphisms. -/
]
def toMulEquiv [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : g.comp f = MonoidHom.id _)
(h₂ : f.comp g = MonoidHom.id _) : M ≃* N where
toFun := f
invFun := g
left_inv := DFunLike.congr_fun h₁
right_inv := DFunLike.congr_fun h₂
map_mul' := f.map_mul
