Commit 2025-08-26 23:57 b5a15dd6

View on Github →

refactor: generalise monotonicity of scalar multiplication to star-semimodules (#28852)

Estimated changes

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

Modified Mathlib/Algebra/Order/Star/Basic.lean

modified theorem StarModule.smul_lt_smul_of_pos

added theorem StarOrderedRing.lt_iff

modified theorem StarOrderedRing.nonneg_iff

modified theorem StarOrderedRing.of_le_iff

added theorem StarOrderedRing.pos_iff

added theorem smul_mem_closure_star_mul

Modified Mathlib/Analysis/RCLike/Basic.lean

added theorem RCLike.toPosMulReflectLT