Def Submodule.toAddSubgroup

Modification history

2023-01-27 18:02

Mathlib/Algebra/Module/Submodule/Basic.lean

feat: port Algebra.Module.Submodule.Basic (#1888)

Added Submodule.toAddSubgroup View on Github →