Theorems · Definition · group theory

zmodAddEquivOfGenerator

{G : Type u_2} →
  [inst : AddGroup G] → {g : G} → (∀ (x : G), x ∈ AddSubgroup.zmultiples g) → {n : ℕ} → Nat.card G = n → ZMod n ≃+ G

The isomorphism from ZMod n to any additive group of Nat.card equal to n generated by a single element g which sends 1 to g. See zmodAddCyclicAddEquiv for a version which doesn't take an explicit generator, and instead picks one out with the axiom of choice.

Defined in

Mathlib.GroupTheory.SpecificGroups.Cyclic

Cited by

5 results in Mathlib

Foundations

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

Assumes

AddGroup