# Documentation

Mathlib.Algebra.Order.Nonneg.Module

# 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} [] [SMul 𝕜 𝕜'] :
SMul 𝕜≥0 𝕜'
Equations
• Nonneg.instSMul = { smul := fun (c : 𝕜≥0) (x : 𝕜') => c x }
@[simp]
theorem Nonneg.coe_smul {𝕜 : Type u_1} {𝕜' : Type u_2} [] [SMul 𝕜 𝕜'] (a : 𝕜≥0) (x : 𝕜') :
a x = a x
@[simp]
theorem Nonneg.mk_smul {𝕜 : Type u_1} {𝕜' : Type u_2} [] [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} [] [SMul 𝕜 𝕜'] [SMul 𝕜 E] [SMul 𝕜' E] [IsScalarTower 𝕜 𝕜' E] :
IsScalarTower 𝕜≥0 𝕜' E
Equations
instance Nonneg.instSMulWithZero {𝕜 : Type u_1} {𝕜' : Type u_2} [] [Zero 𝕜'] [SMulWithZero 𝕜 𝕜'] :
SMulWithZero 𝕜≥0 𝕜'
Equations
instance Nonneg.instOrderedSmul {𝕜 : Type u_1} {E : Type u_3} [] [] [hE : ] :
OrderedSMul 𝕜≥0 E
Equations
instance Nonneg.instModule {𝕜 : Type u_1} {E : Type u_3} [] [] [Module 𝕜 E] :
Module 𝕜≥0 E

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

Equations