Theorems · Definition · group theory

QuotientGroup.quotientQuotientEquivQuotient

• 1000+ list: Isomorphism theorem
• 1000+ list: Lattice theorem

{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

Noether's third isomorphism theorem for groups: (G / N) / (M / N) ≃* G / M.

Defined in

Mathlib.GroupTheory.QuotientGroup.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupSubgroup.NormalSubgroup.Normal