Commit 2024-06-27 04:18 086557dc

View on Github →

feat: Star algebras satisfy OrderedSMul (#13427) This PR shows that star algebras satisfy OrderedSMul 𝕜 A whenever 𝕜 is RCLike and A is a non-unital star algebra.

Estimated changes

Modified Mathlib/Algebra/Star/Order.lean

added theorem StarModule.smul_lt_smul_of_pos

Modified Mathlib/Analysis/RCLike/Basic.lean

added theorem StarModule.instOrderedSMul