Theorem smul_one_strictMono

Modification history

2026-04-01 19:38
Mathlib/Algebra/Order/Module/Defs.lean
chore(Algebra/Order): generalise ordered algebra lemmas (#37040) …
Added smul_one_strictMonoView on Github →