Spans in modules over ℤ/nℤ

In a ZMod n-module, additive generation and linear generation agree. This identifies the group-theoretic generation criterion for an elementary abelian group with a spanning criterion in its associated vector space.

@[simp]

theorem Set.span_zmod_eq_addSubgroupClosure {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module (ZMod n) M] (s : Set M) : (Submodule.span (ZMod n) s).toAddSubgroup = AddSubgroup.closure s

The span over ℤ/nℤ has the same underlying additive subgroup as the subgroup generated by the set. This also includes n = 0, where ZMod 0 = ℤ.