Theorems · Definition · group theory

QuotientGroup.quotientQuotientEquivQuotientAux

{G : Type u} →
  [inst : Group G] →
    (N : Subgroup G) →
      [nN : N.Normal] →
        (M : Subgroup G) → [nM : M.Normal] → N ≤ M → (G ⧸ N) ⧸ Subgroup.map (QuotientGroup.mk' N) M →* G ⧸ M

The map from the third isomorphism theorem for groups: (G / N) / (M / N) → G / M.

Defined in

Mathlib.GroupTheory.QuotientGroup.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

GroupSubgroup.NormalSubgroup.Normal