Theorems · Definition · group theory

AddMonoidHom.toAddEquiv

{M : Type u_4} →
  {N : Type u_5} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] →
        (f : M →+ N) → (g : N →+ M) → g.comp f = AddMonoidHom.id M → f.comp g = AddMonoidHom.id N → M ≃+ N

Given a pair of additive monoid 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 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

AddZeroClassAddZeroClass