Structures · Algebra
PosSMulReflectLT
Typeclass for strict reverse monotonicity of scalar multiplication by nonnegative 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 lt_of_smul_lt_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 by27
- smul_lt_smul_iff_of_pos_left
- lt_of_smul_lt_smul_left
- smul_lt_smul_iff_of_neg_left
- lt_of_smul_lt_smul_of_nonneg_left
- starConvex_compl_Iic
- lineMap_lt_lineMap_iff_of_lt
- pos_of_smul_pos_left
- PosSMulReflectLT.toPosSMulMono
- left_lt_lineMap_iff_lt
- smul_neg_iff_of_neg_left
- lineMap_lt_right_iff_lt
- PosSMulReflectLT.lt_of_smul_lt_smul_left
- smul_pos_iff_of_neg_left
- OrderDual.instPosSMulReflectLT
- pos_iff_pos_of_smul_pos
- right_lt_lineMap_iff_lt
- lt_of_smul_lt_smul_of_nonpos
- smul_pos_iff_of_pos_left
- smul_pos_of_neg_of_neg
- smul_neg_iff_of_pos_left
- starConvex_compl_Ici
- lt_inv_smul_iff_of_pos
- PosSMulReflectLT.toPosSMulReflectLE
- inv_smul_lt_iff_of_pos
- PosSMulReflectLT.lift
- neg_of_smul_neg_left
- lineMap_lt_left_iff_lt
Ancestors0
No ancestors.