Theorems · Definition · group theory

MonoidHom.inverse

{A : Type u_10} →
  {B : Type u_11} →
    [inst : Monoid A] →
      [inst_1 : Monoid B] → (f : A →* B) → (g : B → A) → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → B →* A

The inverse of a bijective MonoidHom is a MonoidHom.

Defined in

Mathlib.Algebra.Group.Hom.Defs

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms

Assumes

MonoidMonoid