English
Let M be an additive group with a Z/n-module structure. There is a canonical isomorphism between AddSubgroups of M and ZMod-submodules of M. The inverse of this isomorphism is the natural forgetful map that sends a ZMod-submodule to its underlying AddSubgroup.
Русский
Пусть M — аддитивная группа с модульной структурой над Z/nZ. Существует каноническое изоморфизм между AddSubgroup(M) и Submodule(ZMod n) M. Обратное этому изоморфизму есть естественный забывающий переход от ZMod-подмодуля к его базовой подгруппе AddSubgroup.
LaTeX
$$$\\big((\\mathrm{toZModSubmodule}(n))\\!\\cdot\\text{symm}\\big) = \\mathrm{Submodule.toAddSubgroup}$$$
Lean4
@[simp]
theorem toZModSubmodule_symm : ⇑((toZModSubmodule n).symm : _ ≃o AddSubgroup M) = Submodule.toAddSubgroup :=
rfl
