Theorems · Definition · group theory

QuotientAddGroup.liftEquiv

{G : Type u_1} →
  {H : Type u_2} →
    [inst : AddGroup G] →
      [inst_1 : AddGroup H] →
        (N : AddSubgroup G) → [nN : N.Normal] → {φ : G →+ H} → Function.Surjective ⇑φ → N = φ.ker → G ⧸ N ≃+ H

A surjective AddGroup homomorphism φ : G →+ H with N = ker(φ) descends (i.e. lifts) to an AddGroup isomorphism G/N ≃+ H.

Defined in

Mathlib.GroupTheory.QuotientGroup.Defs

Cited by

2 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupAddGroupAddSubgroup.Normal