Theorem smul_strictMono_right

Modification history

2024-04-02 23:42
Mathlib/Algebra/Order/Group/Action.lean
feat: pointwise scalar multiplication is monotone (#11809) …
Added smul_strictMono_rightView on Github →