Structures · Algebra
IsOrderedModule
An ordered module is a module with a partial order such that scalar multiplication by a nonnegative scalar and of a nonnegative vector are both monotone.
- Defined in
- Mathlib.Algebra.Order.Module.Defs
- Shape
- 2 explicit arguments
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- NNReal
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by172
- MeasureTheory.integral_nonneg
- HahnEmbedding.Partial
- HahnEmbedding.ArchimedeanStrata.stratum
- MeasureTheory.integral_nonneg_of_ae
- MeasureTheory.integral_mono
- MeasureTheory.integral_mono_of_nonneg
- MeasureTheory.integral_mono_ae
- HahnEmbedding.Partial.eval
- HahnEmbedding.Seed.baseEmbedding
- HahnEmbedding.Seed.toArchimedeanStrata
- MeasureTheory.setIntegral_mono_on
- MeasureTheory.setIntegral_mono_set
- HahnEmbedding.Partial.evalCoeff
- HahnEmbedding.Partial.evalCoeff_eq
- MeasureTheory.condExp_nonneg
- HahnEmbedding.Seed.coeff
- MeasureTheory.condExp_mono
- HahnEmbedding.Partial.sSupFun
- MeasureTheory.setIntegral_mono_ae_restrict
- HahnEmbedding.IsPartial.strictMono
- HahnEmbedding.Partial.extendFun
- MeasureTheory.integral_mono_measure
- MeasureTheory.setIntegral_mono_ae
- HahnEmbedding.IsPartial.baseEmbedding_le
- HahnEmbedding.IsPartial.truncLT_mem_range
- HahnEmbedding.ArchimedeanStrata.baseDomain
- HahnEmbedding.ArchimedeanStrata.ball_sup_stratum_eq
- HahnEmbedding.Partial.evalCoeff_eq_zero
- MeasureTheory.integral_nonpos_of_ae
- HahnEmbedding.ArchimedeanStrata.stratum'
- HahnEmbedding.ArchimedeanStrata.archimedeanClassMk_of_mem_stratum
- HahnEmbedding.Seed.strictMono_coeff
- MeasureTheory.setIntegral_mono
- HahnEmbedding.Seed.coeff_baseEmbedding
- ConvexOn.smul'
- ConvexOn.pow
- HahnEmbedding.Partial.val_sub_ne_zero
- MeasureTheory.Submartingale.expected_stoppedValue_mono
- Real.sInf_smul_of_nonneg
- MeasureTheory.setIntegral_mono_on₀
- MeasureTheory.Submartingale.setIntegral_le
- HahnEmbedding.Partial.le_sSupFun
- HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk
- HahnEmbedding.Partial.extend
- ConcaveOn.smul'
- MeasureTheory.submartingale_of_condExp_sub_nonneg_nat
- HahnEmbedding.Partial.coeff_ne_zero
- ConcaveOn.smul''
- MeasureTheory.Supermartingale.smul_nonneg
- HahnEmbedding.Seed.mem_domain_baseEmbedding