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.
@[simp]
theorem
Nonneg.coe_smul
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[OrderedSemiring 𝕜]
[SMul 𝕜 𝕜']
(a : { c : 𝕜 // 0 ≤ c })
(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 { c : 𝕜 // 0 ≤ c } 𝕜' E
Equations
- (_ : IsScalarTower { c : 𝕜 // 0 ≤ c } 𝕜' E) = (_ : IsScalarTower { x : 𝕜 // 0 ≤ x } 𝕜' E)
instance
Nonneg.instSMulWithZero
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[OrderedSemiring 𝕜]
[Zero 𝕜']
[SMulWithZero 𝕜 𝕜']
:
SMulWithZero { c : 𝕜 // 0 ≤ c } 𝕜'
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 { c : 𝕜 // 0 ≤ c } E
Equations
- (_ : OrderedSMul { c : 𝕜 // 0 ≤ c } E) = (_ : OrderedSMul { c : 𝕜 // 0 ≤ c } E)
instance
Nonneg.instModule
{𝕜 : Type u_1}
{E : Type u_3}
[OrderedSemiring 𝕜]
[AddCommMonoid E]
[Module 𝕜 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