Structures · Algebra
PosSMulReflectLE
Typeclass for reverse monotonicity of scalar multiplication by positive elements on the left,
namely a • b₁ ≤ a • b₂ → b₁ ≤ b₂ if 0 < a.
You should usually not use this very granular typeclass directly, but rather a typeclass like
IsOrderedModule.
- Defined in
- Mathlib.Algebra.Order.Module.Defs
- Shape
- 2 explicit arguments · adds le_of_smul_le_smul_left
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by56
- OrderIso.smulRight
- smul_le_smul_iff_of_pos_left
- le_of_smul_le_smul_left
- le_inv_smul_iff_of_pos
- inv_smul_le_iff_of_pos
- le_of_smul_le_smul_of_pos_left
- map_le_lineMap_iff_slope_le_slope_left
- lineMap_le_right_iff_le
- smul_le_smul_iff_of_neg_left
- map_le_lineMap_iff_slope_le_slope_right
- IsMinOn.of_isLocalMinOn_of_convexOn
- map_le_lineMap_iff_slope_le_slope
- left_le_lineMap_iff_le
- lineMap_le_lineMap_iff_of_lt
- right_le_lineMap_iff_le
- bddBelow_smul_iff_of_pos
- lineMap_le_left_iff_le
- IsMinOn.of_isLocalMin_of_convex_univ
- PosSMulReflectLE.toPosSMulStrictMono
- map_lt_lineMap_iff_slope_lt_slope_left
- smul_ceilDiv
- nonpos_of_smul_nonpos_of_pos_left
- lineMap_le_map_iff_slope_le_slope
- map_lt_lineMap_iff_slope_lt_slope
- bddAbove_smul_iff_of_pos
- nonneg_of_smul_nonneg_of_pos_left
- smul_floorDiv
- IsMinOn.of_isLocalMinOn_of_convexOn_Icc
- lineMap_le_map_iff_slope_le_slope_right
- map_lt_lineMap_iff_slope_lt_slope_right
- lineMap_le_map_iff_slope_le_slope_left
- PosSMulReflectLE.le_of_smul_le_smul_left
- DFinsupp.instPosSMulReflectLE
- right_le_midpoint
- upperBounds_smul_of_pos
- smul_nonneg_iff_nonneg_of_pos_left
- le_of_smul_le_smul_of_neg
- lineMap_lt_map_iff_slope_lt_slope_left
- Pi.instPosSMulReflectLE
- OrderIso.smulRight_symm_apply
- lowerBounds_smul_of_pos
- midpoint_le_right
- Finsupp.instPosSMulReflectLE
- PosSMulReflectLE.toPosSMulReflectLT
- OrderDual.instPosSMulReflectLE
- midpoint_le_left
- IsMaxOn.of_isLocalMax_of_convex_univ
- left_le_midpoint
- OrderIso.smulRight_apply
- PosSMulReflectLE.lift
Ancestors0
No ancestors.