Theorems · Theorem · group theory

Subgroup.index_eq_sum_minimalPeriod

∀ {G : Type u_3} [inst : Group G] (H : Subgroup G) (g : G) [Finite (G ⧸ H)]
  [inst_2 : Fintype (Quotient (MulAction.orbitRel (↥(Subgroup.zpowers g)) (G ⧸ H)))],
  H.index = ∑ q, Function.minimalPeriod (fun x => g • x) q.out

The sum of minimal periods over all orbits equals the index [G:H].

Defined in

Mathlib.Data.ZMod.QuotientGroup

Cited by

3 results in Mathlib

Foundations

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

Assumes

GroupFiniteFintype