Theorem smul_le_smul_left

Modification history

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