Theorems · Theorem · group theory

MonoidHom.independent_range_of_coprime_order

∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Type u_3} [inst_1 : (i : ι) → Group (H i)]
  (ϕ : (i : ι) → H i →* G),
  (Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)) →
    ∀ [Finite ι] [inst_3 : (i : ι) → Fintype (H i)],
      (Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))) → iSupIndep fun i => (ϕ i).range

Defined in

Mathlib.GroupTheory.NoncommPiCoprod

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupGroupFiniteFintype