Commit 2026-08-13 18:50 5b8fb9a6

View on Github →

feat(Analysis/InnerProductSpace/Positive): add IsOrderedModule for (Continuous)LinearMaps (#42680) This PR adds the instance IsOrderedModule and the pre-requisite AddLeftMono and AddRightMono for linear maps and continuous linear maps from an inner product space to itself.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

modified theorem ContinuousLinearMap.coe_le_coe_iff

modified theorem ContinuousLinearMap.le_def

modified theorem ContinuousLinearMap.nonneg_iff_isPositive

modified theorem LinearMap.le_def

modified theorem LinearMap.nonneg_iff_isPositive

Modified Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean