Theorems · Definition · group theory

MulHom.toMulEquiv

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

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.

Defined in

Mathlib.Algebra.Group.Equiv.Defs

Cited by

2 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext

Assumes

MulMul