Theorems · Theorem · group theory

Monoid.CoprodI.lift_word_prod_nontrivial_of_head_card

∀ {ι : Type u_1} {G : Type u_4} [inst : Group G] {H : ι → Type u_5} [inst_1 : (i : ι) → Group (H i)]
  (f : (i : ι) → H i →* G) {α : Type u_6} [inst_2 : MulAction G α] (X : ι → Set α),
  (∀ (i : ι), (X i).Nonempty) →
    Pairwise (Function.onFun Disjoint X) →
      (Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i) →
        ∀ [Nontrivial ι] {i j : ι} (w : Monoid.CoprodI.NeWord H i j),
          3 ≤ Cardinal.mk (H i) → i ≠ j → (Monoid.CoprodI.lift f) w.prod ≠ 1

Defined in

Mathlib.GroupTheory.CoprodI

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupGroupMulActionNontrivial