Modules over nonnegative elements #

This file defines instances and prove some properties about modules over nonnegative elements {c : 𝕜 // 0 ≤ c} of an arbitrary OrderedSemiring 𝕜.

These instances are useful for working with ConvexCone.

instance Nonneg.instSMul {𝕜 : Type u_1} {𝕜' : Type u_2} [OrderedSemiring 𝕜] [SMul 𝕜 𝕜'] :
SMul 𝕜≥0 𝕜'
  • Nonneg.instSMul = { smul := fun (c : 𝕜≥0) (x : 𝕜') => c x }
theorem Nonneg.coe_smul {𝕜 : Type u_1} {𝕜' : Type u_2} [OrderedSemiring 𝕜] [SMul 𝕜 𝕜'] (a : 𝕜≥0) (x : 𝕜') :
a x = a x
theorem Nonneg.mk_smul {𝕜 : Type u_1} {𝕜' : Type u_2} [OrderedSemiring 𝕜] [SMul 𝕜 𝕜'] (a : 𝕜) (ha : 0 a) (x : 𝕜') :
{ val := a, property := ha } x = a x
instance Nonneg.instIsScalarTower {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [SMul 𝕜 𝕜'] [SMul 𝕜 E] [SMul 𝕜' E] [IsScalarTower 𝕜 𝕜' E] :
IsScalarTower 𝕜≥0 𝕜' E
instance Nonneg.instSMulWithZero {𝕜 : Type u_1} {𝕜' : Type u_2} [OrderedSemiring 𝕜] [Zero 𝕜'] [SMulWithZero 𝕜 𝕜'] :
SMulWithZero 𝕜≥0 𝕜'
instance Nonneg.instOrderedSmul {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [OrderedAddCommMonoid E] [SMulWithZero 𝕜 E] [hE : OrderedSMul 𝕜 E] :
OrderedSMul 𝕜≥0 E
instance Nonneg.instModule {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] :
Module 𝕜≥0 E

A module over an ordered semiring is also a module over just the non-negative scalars.