Cyclic groups

For n ≠ 0, this file gives the standard computable enumeration of Multiplicative (ZMod n), transported from the additive group ZMod n. It also records that an element corresponding to 1 under an equivalence with Multiplicative ℤ generates its group.

Main definitions

• TauCeti.cyclicElements: a computable enumeration of Multiplicative (ZMod n).

Main results

• TauCeti.mem_cyclicElements: the enumeration exhausts the group when n ≠ 0.
• MulEquiv.zpowers_eq_top_of_apply_eq_ofAdd_one: an element sent to 1 by an equivalence with Multiplicative ℤ generates its group.

References

The construction follows the enumeration pattern of TauCeti.dihedralElements.

def TauCeti.cyclicElements (n : ℕ) : List (Multiplicative (ZMod n))

For n ≠ 0, the standard computable enumeration of the finite cyclic group Multiplicative (ZMod n). For n = 0, this list is empty.

Equations

• TauCeti.cyclicElements n = List.ofFn fun (i : Fin n) => Multiplicative.ofAdd ↑↑i

theorem TauCeti.mem_cyclicElements (n : ℕ) [NeZero n] (g : Multiplicative (ZMod n)) : g ∈ cyclicElements n

Every element of Multiplicative (ZMod n) occurs in TauCeti.cyclicElements n when n is nonzero.

theorem MulEquiv.zpowers_eq_top_of_apply_eq_ofAdd_one {G : Type u_1} [Group G] {g : G} (e : G ≃* Multiplicative ℤ) (hg : e g = Multiplicative.ofAdd 1) : Subgroup.zpowers g = ⊤

An element sent to 1 by a group equivalence with Multiplicative ℤ generates its group.