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.

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