Documentation

Mathlib.Algebra.Order.Nonneg.Module

Modules over nonnegative elements #

For an ordered ring R, this file proves that any (ordered) R-module M is also an (ordered) R≥0-module`.

Among other things, these instances are useful for working with ConvexCone.

source
instance Nonneg.instSMul {R : Type u_1} {S : Type u_2} [Semiring R] [PartialOrder R] [SMul R S] :
SMul { c : R // 0 ≤ c } S
Equations
source
@[simp]
theorem Nonneg.coe_smul {R : Type u_1} {S : Type u_2} [Semiring R] [PartialOrder R] [SMul R S] (a : { c : R // 0 ≤ c }) (x : S) :
↑a • x = a • x
source
@[simp]
theorem Nonneg.mk_smul {R : Type u_1} {S : Type u_2} [Semiring R] [PartialOrder R] [SMul R S] (a : R) (ha : 0 ≤ a) (x : S) :
⟨a, ha⟩ • x = a • x
source
instance Nonneg.instIsScalarTower {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [SMul R S] [SMul R M] [SMul S M] [IsScalarTower R S M] :
IsScalarTower { c : R // 0 ≤ c } S M
source
instance Nonneg.instSMulWithZero {R : Type u_1} {S : Type u_2} [Semiring R] [PartialOrder R] [Zero S] [SMulWithZero R S] :
SMulWithZero { c : R // 0 ≤ c } S
Equations
source
instance Nonneg.instOrderedSMul {R : Type u_1} {M : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid M] [PartialOrder M] [SMulWithZero R M] [hE : OrderedSMul R M] :
OrderedSMul { c : R // 0 ≤ c } M
source
instance Nonneg.instModule {R : Type u_1} {M : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid M] [Module R M] :
Module { c : R // 0 ≤ c } M

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

Equations