Theorem smul_iInf_le

Modification history

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