Theorems · Theorem · group theory

Subgroup.quotientEquivSigmaZMod_apply

∀ {G : Type u_3} [inst : Group G] (H : Subgroup G) (g : G)
  (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H)) (k : ℤ),
  (H.quotientEquivSigmaZMod g) (g ^ k • Quotient.out q) = ⟨q, ↑k⟩

Defined in

Mathlib.Data.ZMod.QuotientGroup

Cited by

1 results in Mathlib

Foundations

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

Assumes

Group