Theorem Submodule.top_toAddSubgroup

Modification history

2024-01-06 09:51
Mathlib/Algebra/Module/Submodule/Lattice.lean
feat: Provide glue between `AddCommGroup` and `Module ℤ` (#9345)
Added Submodule.top_toAddSubgroupView on Github →