Theorems · Theorem · group theory

MonoidHom.injective_noncommPiCoprod_of_iSupIndep

∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Type u_3} [inst_1 : (i : ι) → Group (H i)]
  (ϕ : (i : ι) → H i →* G) [inst_2 : Fintype ι]
  {hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)},
  (iSupIndep fun i => (ϕ i).range) →
    (∀ (i : ι), Function.Injective ⇑(ϕ i)) → Function.Injective ⇑(MonoidHom.noncommPiCoprod ϕ hcomm)

Defined in

Mathlib.GroupTheory.NoncommPiCoprod

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupGroupFintype