Theorem StarModule.instOrderedSMul

Modification history

2024-06-27 04:18

Mathlib/Analysis/RCLike/Basic.lean

feat: Star algebras satisfy `OrderedSMul` (#13427) …

Added StarModule.instOrderedSMul View on Github →