Structures · Algebra
SMulPosStrictMono
Typeclass for strict monotonicity of scalar multiplication by positive elements on the left,
namely a₁ < a₂ → a₁ • b < a₂ • b if 0 < b.
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 smul_lt_smul_of_pos_right
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances3
- Int
- Nat
- NNReal
How is a type an instance?
Loading the hierarchy index…
Assumed by33
- smul_lt_smul_of_pos_right
- smul_lt_smul_iff_of_pos_right
- strictMono_smul_right_of_pos
- algebraMap_strictMono
- smul_neg_of_neg_of_pos
- SMulPosStrictMono.smul_lt_smul_of_pos_right
- smul_one_strictMono
- SMulPosStrictMono.lift
- NNReal.instSMulPosStrictMono
- SMulPosStrictMono.toSMulPosReflectLE
- OrderDual.instSMulPosStrictMono
- smul_lt_smul_of_lt_of_le
- smul_eq_smul_iff_eq_and_eq_of_pos
- smul_lt_iff_lt_one_left
- smul_pos_iff_of_pos_right
- smul_eq_smul_iff_eq_and_eq_of_pos'
- SMulPosStrictMono.toSMulPosMono
- algebraMap_lt_algebraMap
- Finsupp.instSMulPosStrictMono
- DFinsupp.instSMulPosStrictMono
- smul_lt_smul_of_lt_of_le'
- lt_smul_iff_one_lt_left
- StrictAnti.smul_const
- lt_smul_of_one_lt_left
- openSegment.lift
- Pi.instSMulPosStrictMono
- StrictMono.smul_const
- smul_pos'
- smul_lt_smul
- smul_lt_of_lt_one_left
- Prod.instSMulPosStrictMono
- smul_lt_smul'
- algebraMap_pos
Ancestors0
No ancestors.