Theorems · Definition · group theory

MonoidHom.toMulEquiv

{M : Type u_4} →
  {N : Type u_5} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] →
        (f : M →* N) → (g : N →* M) → g.comp f = MonoidHom.id M → f.comp g = MonoidHom.id N → M ≃* N

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.

Defined in

Mathlib.Algebra.Group.Equiv.Defs

Cited by

3 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound

Assumes

MulOneClassMulOneClass