Theorems · Theorem · group theory

QuotientGroup.map_id_apply

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

Defined in

Mathlib.GroupTheory.QuotientGroup.Defs

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupSubgroup.Normal