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

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

Equations