Lean4
/-- Given a pair of multiplicative 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 multiplicative
homomorphisms. -/
@[to_additive (attr := simps -fullyApplied) /--
Given a pair of additive 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
homomorphisms. -/
]
def toMulEquiv [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : g.comp f = MulHom.id _) (h₂ : f.comp g = MulHom.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
