Theorems · Theorem · group theory

QuotientGroup.map_id

∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal]
  (h : optParam (N ≤ Subgroup.comap (MonoidHom.id G) N) ⋯),
  QuotientGroup.map N N (MonoidHom.id G) h = MonoidHom.id (G ⧸ N)

Defined in

Mathlib.GroupTheory.QuotientGroup.Defs

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupSubgroup.Normal