Structures · Algebra
IsStrictOrderedModule
An ordered module is a module with a partial order such that scalar multiplication by a positive scalar and of a positive vector are both strictly monotone.
- Defined in
- Mathlib.Algebra.Order.Module.Defs
- Shape
- 2 explicit arguments
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances4
- Rat
- NNReal
- NNRat
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by118
- ConvexOn.map_sum_le
- gauge_smul_of_nonneg
- ConvexOn.exists_ge_of_mem_convexHull
- lineMap_lt_lineMap_iff_of_lt'
- StrictConvexOn.map_sum_eq_iff
- monovaryOn_iff_forall_smul_nonneg
- lineMap_le_lineMap_iff_of_lt'
- ConvexOn.map_centerMass_le
- StrictConvexOn.eq_of_le_map_sum
- ConvexOn.smul'
- StrictConvexOn.map_sum_lt
- map_le_lineMap_iff_slope_le_slope_left
- ConvexOn.le_max_of_mem_segment
- monovaryOn_iff_smul_rearrangement
- ConcaveOn.smul'
- StrictConvexOn.map_sum_eq_iff_of_pos
- ConcaveOn.smul''
- lineMap_mono_left
- ConvexOn.map_add_sum_le
- lineMap_le_right_iff_le
- map_le_lineMap_iff_slope_le_slope_right
- StrictConvexOn.map_sum_lt_iff_of_pos'
- monovary_iff_forall_smul_nonneg
- starConvex_compl_Iic
- ConvexOn.exists_ge_of_centerMass
- map_le_lineMap_iff_slope_le_slope
- ConvexOn.smul''
- midpoint_le_midpoint
- ConvexOn.bddAbove_convexHull
- monovary_iff_smul_rearrangement
- lineMap_lt_lineMap_iff_of_lt
- left_le_lineMap_iff_le
- lineMap_le_lineMap_iff_of_lt
- right_le_lineMap_iff_le
- StrictConvexOn.map_sum_lt_iff_of_nonneg
- lineMap_le_left_iff_le
- ConcaveOn.smul_convexOn'
- lineMap_strict_mono_right
- gauge_smul_left
- map_lt_lineMap_iff_slope_lt_slope_left
- MonovaryOn.smul_add_smul_le_smul_add_smul
- lineMap_mono_endpoints
- antivaryOn_iff_forall_smul_nonpos
- ConvexOn.le_sup_of_mem_convexHull
- gauge_smul_left_of_nonneg
- lineMap_le_map_iff_slope_le_slope
- left_lt_lineMap_iff_lt
- antivary_iff_forall_smul_nonpos
- map_lt_lineMap_iff_slope_lt_slope
- AntivaryOn.smul_add_smul_le_smul_add_smul