Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes