Theorems · Theorem · group theory

Subgroup.noncommPiCoprod_range

∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Subgroup G} [inst_1 : Fintype ι]
  {hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y},
  (Subgroup.noncommPiCoprod hcomm).range = ⨆ i, H i

Defined in

Mathlib.GroupTheory.NoncommPiCoprod

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupFintype