Theorems · Definition · group theory

QuotientAddGroup.quotientMapAddSubgroupOfOfLe

{G : Type u} →
  [inst : AddGroup G] →
    {A' A B' B : AddSubgroup G} →
      [_hAN : (A'.addSubgroupOf A).Normal] →
        [_hBN : (B'.addSubgroupOf B).Normal] → A' ≤ B' → A ≤ B → ↥A ⧸ A'.addSubgroupOf A →+ ↥B ⧸ B'.addSubgroupOf 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

AddGroupAddSubgroup.NormalAddSubgroup.Normal