Theorems · Theorem · group theory

Subgroup.noncommPiCoprod_apply

∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Subgroup G} [inst_1 : Fintype ι]
  (comm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y) (u : (i : ι) → ↥(H i)),
  (Subgroup.noncommPiCoprod comm) u = Finset.univ.noncommProd (fun i => ↑(u i)) ⋯

Defined in

Mathlib.GroupTheory.NoncommPiCoprod

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupFintype