Def AddSubgroup.toIntSubmodule

Modification history

2023-02-12 15:02

Mathlib/Algebra/Module/Submodule/Lattice.lean

chore: tidy various files (#2236)

Modified AddSubgroup.toIntSubmodule View on Github →

2023-01-28 21:17

Mathlib/Algebra/Module/Submodule/Lattice.lean

feat: port Algebra.Module.Submodule.Lattice (#1898)

Added AddSubgroup.toIntSubmodule View on Github →