Theorems · Definition · group theory

QuotientAddGroup.quotientQuotientEquivQuotient

{G : Type u} →
  [inst : AddGroup G] →
    (N : AddSubgroup G) →
      [nN : N.Normal] →
        (M : AddSubgroup G) → [nM : M.Normal] → N ≤ M → (G ⧸ N) ⧸ AddSubgroup.map (QuotientAddGroup.mk' N) M ≃+ G ⧸ M

Noether's third isomorphism theorem for additive groups: (A / N) / (M / N) ≃+ A / M.

Defined in

Mathlib.GroupTheory.QuotientGroup.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddGroupAddSubgroup.NormalAddSubgroup.Normal