Theorem Submodule.restrictScalars_monotone

Modification history

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_monotoneView on Github →