The exponent of a group whose additive copy is a ℤ/nℤ-module

Scalars from ZMod n act on a ZMod n-module, so n kills it. Written multiplicatively, a commutative group whose additive copy carries a ZMod n-module structure therefore has exponent dividing n; for a prime n it is elementary abelian. This is the converse of AddCommGroup.zmodModule, which builds the module structure out of that divisibility, and it is what recovers the group-theoretic hypothesis from a module structure that some other construction supplied. The additive form is the same statement, through AddMonoid.exponent_additive.

Main results

• TauCeti.exponent_dvd_of_module_zmod: a commutative group whose additive copy is a ZMod n-module has exponent dividing n.

theorem TauCeti.exponent_dvd_of_module_zmod {n : ℕ} {W : Type u_1} [CommGroup W] [Module (ZMod n) (Additive W)] : Monoid.exponent W ∣ n

A commutative group whose additive copy is a ZMod n-module has exponent dividing n, since n kills every ZMod n-module.