English
The inverse of a bijective MonoidHom is a MonoidHom: if f: A →* B is bijective with inverse g: B → A, then g is a MonoidHom.
Русский
Обратный гомоморфизм моноида к биективному гомоморфизму f: A →* B является MonoidHom.
LaTeX
$$MonoidHom.inverse f g h₁ h₂$$
Lean4
/-- The inverse of a bijective `MonoidHom` is a `MonoidHom`. -/
@[to_additive (attr := simps) /-- The inverse of a bijective `AddMonoidHom` is an `AddMonoidHom`. -/
]
def inverse {A B : Type*} [Monoid A] [Monoid B] (f : A →* B) (g : B → A) (h₁ : Function.LeftInverse g f)
(h₂ : Function.RightInverse g f) : B →* A :=
{ (f : OneHom A B).inverse g h₁, (f : A →ₙ* B).inverse g h₁ h₂ with toFun := g }
