Theorems · Theorem · group theory

Subgroup.pairwiseDisjoint_leftCoset_cover_of_sum_inv_index_eq_one

∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
  ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
    ∀ [inst_1 : DecidablePred Subgroup.FiniteIndex],
      ∑ i ∈ s, (↑(H i).index)⁻¹ = 1 → (↑({i ∈ s | (H i).FiniteIndex})).PairwiseDisjoint fun i => g i • ↑(H i)

Let the group G be the union of finitely many left cosets g i • H i. If the sum of the inverses of the indexes of the subgroups H i is equal to 1, then the cosets of the subgroups of finite index are pairwise disjoint.

Defined in

Mathlib.GroupTheory.CosetCover

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupDecidablePred