Theorem abs_qsmul

Modification history

2025-06-24 23:05
Mathlib/Algebra/Order/Module/Rat.lean
feat(Algebra/Order): more general version of `abs_qsmul` (#26179) …
Modified abs_qsmulView on Github →
2024-07-30 16:56
Mathlib/Algebra/Order/Module/Rat.lean
feat: Monotonicity of multiplication by positive rationals (#15328) …
Added abs_qsmulView on Github →