Commit 2025-09-06 04:27 759a9848

View on Github →

chore: deprecate OrderedSMul (#28817) I follow the pattern of IsOrderedRing/IsStrictOrderedRing by introducing two analogous typeclasses IsOrderedModule/IsStrictOrderedModule.

Estimated changes

modified theorem ConcaveOn.smul'
modified theorem ConcaveOn.smul_convexOn
modified theorem ConvexOn.smul''
modified theorem ConvexOn.smul_concaveOn'
deleted theorem RCLike.toOrderedSMul
deleted theorem ConvexCone.to_orderedSMul