Commit 2021-10-30 09:45 5ff850b9
View on Github →feat(algebra/module/submodule_lattice): add add_subgroup.to_int_submodule (#10051)
This converts an add_subgroup M to a submodule ℤ M. We already have the analogous construction for add_submonoid M.