Theorems · Definition · group theory

QuotientGroup.quotientInfEquivProdNormalQuotient

• 1000+ list: Isomorphism theorem

{G : Type u} →
  [inst : Group G] → (H N : Subgroup G) → [hN : N.Normal] → ↥H ⧸ N.subgroupOf H ≃* ↥(H ⊔ N) ⧸ N.subgroupOf (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 (HN)/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

GroupSubgroup.Normal