Theorem OrderedSMul.mk''

Modification history

2026-03-02 15:01

Mathlib/Algebra/Order/Module/OrderedSMul.lean

chore: delete deprecated modules to end August 2025 (#35873)

Deleted OrderedSMul.mk''View on Github →

2025-04-04 17:16

Mathlib/Algebra/Order/Module/OrderedSMul.lean

chore: use mixin ordered algebraic typeclasses (part 1) (#20594)

Modified OrderedSMul.mk''View on Github →

2023-12-23 10:52

Mathlib/Algebra/Order/Module/OrderedSMul.lean

refactor: Deduplicate monotonicity of `•` lemmas (#9179) …

Modified OrderedSMul.mk''View on Github →

2023-01-16 20:07

Mathlib/Algebra/Order/SMul.lean

feat: port Algebra.Order.SMul (#1553)

Added OrderedSMul.mk''View on Github →