Theorems · Theorem · group theory

Subgroup.quotientEquivSigmaZMod_symm_apply

∀ {G : Type u_3} [inst : Group G] (H : Subgroup G) (g : G)
  (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H))
  (k : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out q))),
  (H.quotientEquivSigmaZMod g).symm ⟨q, k⟩ = g ^ k.cast • Quotient.out q

Defined in

Mathlib.Data.ZMod.QuotientGroup

Cited by

3 results in Mathlib

Foundations

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

Assumes

Group