Theorems · Theorem · group theory

intEquivOfZPowersEqTop_apply

∀ {G : Type u_2} [inst : Infinite G] [inst_1 : Group G] (g : G) (hg : Subgroup.zpowers g = ⊤) (a : Multiplicative ℤ),
  (intEquivOfZPowersEqTop g hg) a = g ^ Multiplicative.toAdd a

Defined in

Mathlib.GroupTheory.SpecificGroups.Cyclic

Cited by

2 results in Mathlib

Foundations

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

Assumes

InfiniteGroup