Def Submodule.restrictScalars

Modification history

2024-01-15 21:28

Mathlib/Algebra/Module/Submodule/Basic.lean

chore: gather results about `Submodule.restrictScalars` into new file (#9765) …

Modified Submodule.restrictScalars View on Github →

2023-03-18 10:25

Mathlib/Algebra/Module/Submodule/Basic.lean

refactor: rename instances in `Algebra.Module.Submodule.Basic` (#2967)

Modified Submodule.restrictScalars View on Github →

2023-01-27 18:02

Mathlib/Algebra/Module/Submodule/Basic.lean

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

Added Submodule.restrictScalars View on Github →