Theorem Submodule.restrictScalars_lt

Modification history

2026-05-25 19:08
Mathlib/Algebra/Module/Submodule/RestrictScalars.lean
feat(Geometry/Convex/Cone): Minor additions to pointed cones (#37464) …
Modified Submodule.restrictScalars_ltView on Github →
2026-01-12 23:59
Mathlib/Algebra/Module/Submodule/RestrictScalars.lean
feat(Algebra/Module/Submodule): behaviour of `restrictScalars` under lattice operations (#33761) …
Added Submodule.restrictScalars_ltView on Github →