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 𝕜'
@[simp]
theorem
Nonneg.coe_smul
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[OrderedSemiring 𝕜]
[SMul 𝕜 𝕜']
(a : 𝕜≥0)
(x : 𝕜')
:
@[simp]
theorem
Nonneg.mk_smul
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[OrderedSemiring 𝕜]
[SMul 𝕜 𝕜']
(a : 𝕜)
(ha : 0 ≤ 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
Equations
- (_ : IsScalarTower 𝕜≥0 𝕜' E) = (_ : IsScalarTower 𝕜≥0 𝕜' E)
instance
Nonneg.instSMulWithZero
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[OrderedSemiring 𝕜]
[Zero 𝕜']
[SMulWithZero 𝕜 𝕜']
:
SMulWithZero 𝕜≥0 𝕜'
Equations
- Nonneg.instSMulWithZero = SMulWithZero.mk (_ : ∀ (x : 𝕜'), 0 • x = 0)
instance
Nonneg.instOrderedSmul
{𝕜 : Type u_1}
{E : Type u_3}
[OrderedSemiring 𝕜]
[OrderedAddCommMonoid E]
[SMulWithZero 𝕜 E]
[hE : OrderedSMul 𝕜 E]
:
OrderedSMul 𝕜≥0 E
Equations
- (_ : OrderedSMul 𝕜≥0 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.
Equations
- Nonneg.instModule = Module.compHom E Nonneg.coeRingHom