Theorems · Definition · group theory

QuotientGroup.quotientMapSubgroupOfOfLe

{G : Type u} →
  [inst : Group G] →
    {A' A B' B : Subgroup G} →
      [_hAN : (A'.subgroupOf A).Normal] →
        [_hBN : (B'.subgroupOf B).Normal] → A' ≤ B' → A ≤ B → ↥A ⧸ A'.subgroupOf A →* ↥B ⧸ B'.subgroupOf B

Let A', A, B', B be subgroups of G. If A' ≤ B' and A ≤ B, then there is a map A / (A' ⊓ A) →* B / (B' ⊓ B) induced by the inclusions.

Defined in

Mathlib.GroupTheory.QuotientGroup.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupSubgroup.NormalSubgroup.Normal