Commit 2026-01-12 23:59 6b2df18e

View on Github →

feat(Algebra/Module/Submodule): behaviour of restrictScalars under lattice operations (#33761) Add lemmas about how restrictScalars interacts with sup, inf, sSup, sInf, iSup and iInf.

Estimated changes

Modified Mathlib/Algebra/Module/Submodule/RestrictScalars.lean

added theorem Submodule.restrictScalars_iInf

added theorem Submodule.restrictScalars_iSup

added theorem Submodule.restrictScalars_inf

added theorem Submodule.restrictScalars_le

added theorem Submodule.restrictScalars_lt

added theorem Submodule.restrictScalars_mono

added theorem Submodule.restrictScalars_monotone

added theorem Submodule.restrictScalars_sInf

added theorem Submodule.restrictScalars_sSup

added theorem Submodule.restrictScalars_sup