Lines and cyclic subgroups in a ZMod n-module

In a module over ZMod n the ZMod n-multiples of a vector z are exactly its ℤ-multiples, since an integer multiple only depends on the residue of the integer. Consequently the line ZMod n ∙ z and the cyclic subgroup generated by z inside the multiplicative copy of the module have the same underlying set, which is what lets a span computation be read as a membership in Subgroup.zpowers and back.

Main results

• TauCeti.toAddSubgroup'_zpowers_ofAdd_eq_span: the cyclic subgroup generated by Multiplicative.ofAdd z, read back as an additive subgroup, is the line ZMod n ∙ z.

theorem TauCeti.toAddSubgroup'_zpowers_ofAdd_eq_span {n : ℕ} {V : Type u_1} [AddCommGroup V] [Module (ZMod n) V] (z : V) : Subgroup.toAddSubgroup' (Subgroup.zpowers (Multiplicative.ofAdd z)) = (ZMod n ∙ z).toAddSubgroup

A cyclic subgroup of a ZMod n-module is a line. Read through Multiplicative, the subgroup generated by z consists of the ZMod n-multiples of z.