Theorems · Theorem · group theory

QuotientGroup.ker_lift

∀ {G : Type u_1} {M : Type u_4} [inst : Group G] [inst_1 : Monoid M] (N : Subgroup G) [nN : N.Normal] (φ : G →* M)
  (HN : N ≤ φ.ker), (QuotientGroup.lift N φ HN).ker = Subgroup.map (QuotientGroup.mk' N) φ.ker

Defined in

Mathlib.GroupTheory.QuotientGroup.Defs

Cited by

3 results in Mathlib

Foundations

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

Assumes

GroupMonoidSubgroup.Normal