Theorems · Definition · group theory

QuotientGroup.quotientInfEquivProdNormalizerQuotient

{G : Type u} →
  [inst : Group G] →
    (H N : Subgroup G) → (hLE : H ≤ Subgroup.normalizer ↑N) → ↥H ⧸ N.subgroupOf H ≃* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)

Noether's second isomorphism theorem: given a subgroup N of G and a subgroup H of the normalizer of N in G, defines an isomorphism between H/(H ∩ N) and (HN)/N.

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

Group