Commit 2025-08-26 15:11 483880a5

View on Github →

chore: generalise OrderedSMul to PosSMulMono/PosSMulStrictMono (#28902) ... when in a semimodule.

Estimated changes

Modified Mathlib/Algebra/Order/Chebyshev.lean

Modified Mathlib/Algebra/Order/Module/Defs.lean

Modified Mathlib/Analysis/Convex/Basic.lean

modified theorem Set.OrdConnected.convex

modified theorem Set.OrdConnected.convex_of_chain

Modified Mathlib/Analysis/Convex/Combination.lean

Modified Mathlib/Analysis/Convex/Function.lean

Modified Mathlib/Analysis/Convex/Piecewise.lean

Modified Mathlib/Analysis/Convex/Quasiconvex.lean

Modified Mathlib/Analysis/Convex/Segment.lean

Modified Mathlib/Analysis/Convex/Star.lean

modified theorem Set.OrdConnected.starConvex

Modified Mathlib/Analysis/Convex/Strict.lean