Theorems · Theorem · group theory

QuotientGroup.map_map

∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (N : Subgroup G) [nN : N.Normal] {I : Type u_5}
  [inst_2 : Group I] (M : Subgroup H) (O : Subgroup I) [inst_3 : M.Normal] [inst_4 : O.Normal] (f : G →* H) (g : H →* I)
  (hf : N ≤ Subgroup.comap f M) (hg : M ≤ Subgroup.comap g O) (hgf : optParam (N ≤ Subgroup.comap (g.comp f) O) ⋯)
  (x : G ⧸ N), (QuotientGroup.map M O g hg) ((QuotientGroup.map N M f hf) x) = (QuotientGroup.map N O (g.comp f) hgf) 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

GroupGroupSubgroup.NormalGroupSubgroup.NormalSubgroup.Normal