Theorems · Definition · group theory

QuotientAddGroup.quotientInfEquivSumNormalQuotient

{G : Type u} →
  [inst : AddGroup G] →
    (H N : AddSubgroup G) → [hN : N.Normal] → ↥H ⧸ N.addSubgroupOf H ≃+ ↥(H ⊔ N) ⧸ N.addSubgroupOf (H ⊔ N)

Noether's second isomorphism theorem: given two subgroups H and N of a group G, where N is normal, defines an isomorphism between H/(H ∩ N) and (H + N)/N.

Defined in

Mathlib.GroupTheory.QuotientGroup.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddGroupAddSubgroup.Normal