Theorem smul_inf_le

Modification history

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