English
If every element in an abelian group G has order dividing n, then G carries a natural ZMod n-module structure; for n = 0 this reduces to the integer-module structure.
Русский
Если каждый элемент абелевой группы G имеет порядок делимый на n, то G естественным образом становится ZMod n-модулем; при n = 0 это сводится к целочисленной модульной структуре.
LaTeX
$$$\\operatorname{zmodModule}(G, n, h)$$$
Lean4
/-- The `ZMod n`-module structure on Abelian groups whose elements have order dividing `n`.
See note [reducible non-instances]. -/
abbrev zmodModule {G : Type*} [AddCommGroup G] (h : ∀ (x : G), n • x = 0) : Module (ZMod n) G :=
match n with
| 0 => AddCommGroup.toIntModule G
| _ + 1 => AddCommMonoid.zmodModule h
