Theorems · Definition · group theory

Subgroup.quotientEquivSigmaZMod

{G : Type u_3} →
  [inst : Group G] →
    (H : Subgroup G) →
      (g : G) →
        G ⧸ H ≃
          (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H)) ×
            ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out q))

Partition G ⧸ H into orbits of the action of g : G.

Defined in

Mathlib.Data.ZMod.QuotientGroup

Cited by

7 results in Mathlib

Foundations

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

Assumes

Group