Theorems · Definition · group theory

Subgroup.noncommPiCoprod

{G : Type u_1} →
  [inst : Group G] →
    {ι : Type u_2} →
      {H : ι → Subgroup G} →
        [Fintype ι] → (Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y) → ((i : ι) → ↥(H i)) →* G

The canonical homomorphism from a family of subgroups where elements from different subgroups commute

Defined in

Mathlib.GroupTheory.NoncommPiCoprod

Cited by

12 results in Mathlib

Foundations

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

Assumes

GroupFintype