Mathlib Changelog
v4
Changelog
About
Github
Def
Submodule.restrictScalarsLatticeHom
Modification history
2024-01-16 21:01
Mathlib/Algebra/Module/Submodule/RestrictScalars.lean
feat: basic theory connecting `R[X]`-submodules and invariant `R`-submodules (#9721)
Added
Submodule.restrictScalarsLatticeHom
View on Github →