# Documentation

Mathlib.Algebra.Order.SMul

# Ordered scalar product #

In this file we define

• OrderedSMul R M : an ordered additive commutative monoid M is an OrderedSMul over an OrderedSemiring R if the scalar product respects the order relation on the monoid and on the ring. There is a correspondence between this structure and convex cones, which is proven in Analysis/Convex/Cone.lean.

## Implementation notes #

• We choose to define OrderedSMul as a Prop-valued mixin, so that it can be used for actions, modules, and algebras (the axioms for an "ordered algebra" are exactly that the algebra is ordered as a module).
• To get ordered modules and ordered vector spaces, it suffices to replace the OrderedAddCommMonoid and the OrderedSemiring as desired.

## References #

• https://en.wikipedia.org/wiki/Ordered_module

## Tags #

ordered module, ordered scalar, ordered smul, ordered action, ordered vector space

class OrderedSMul (R : Type u_1) (M : Type u_2) [] [] :
• smul_lt_smul_of_pos : ∀ {a b : M} {c : R}, a < b0 < cc a < c b

Scalar multiplication by positive elements preserves the order.

• lt_of_smul_lt_smul_of_pos : ∀ {a b : M} {c : R}, c a < c b0 < ca < b

If c • a < c • b for some positive c, then a < b.

The ordered scalar product property is when an ordered additive commutative monoid with a partial order has a scalar multiplication which is compatible with the order.

Instances
instance OrderDual.OrderDual.instSMulWithZero {R : Type u_3} {M : Type u_4} [Zero R] [] [] :
instance OrderDual.OrderDual.instMulAction {R : Type u_3} {M : Type u_4} [] [] :
theorem smul_lt_smul_of_pos {R : Type u_3} {M : Type u_4} [] [] [] {a : M} {b : M} {c : R} :
a < b0 < cc a < c b
theorem smul_le_smul_of_nonneg {R : Type u_3} {M : Type u_4} [] [] [] {a : M} {b : M} {c : R} (h₁ : a b) (h₂ : 0 c) :
c a c b
theorem smul_nonneg {R : Type u_3} {M : Type u_4} [] [] [] {a : M} {c : R} (hc : 0 c) (ha : 0 a) :
0 c a
theorem smul_nonpos_of_nonneg_of_nonpos {R : Type u_3} {M : Type u_4} [] [] [] {a : M} {c : R} (hc : 0 c) (ha : a 0) :
c a 0
theorem eq_of_smul_eq_smul_of_pos_of_le {R : Type u_3} {M : Type u_4} [] [] [] {a : M} {b : M} {c : R} (h₁ : c a = c b) (hc : 0 < c) (hle : a b) :
a = b
theorem lt_of_smul_lt_smul_of_nonneg {R : Type u_3} {M : Type u_4} [] [] [] {a : M} {b : M} {c : R} (h : c a < c b) (hc : 0 c) :
a < b
theorem smul_lt_smul_iff_of_pos {R : Type u_3} {M : Type u_4} [] [] [] {a : M} {b : M} {c : R} (hc : 0 < c) :
c a < c b a < b
theorem smul_pos_iff_of_pos {R : Type u_3} {M : Type u_4} [] [] [] {a : M} {c : R} (hc : 0 < c) :
0 < c a 0 < a
theorem smul_pos {R : Type u_3} {M : Type u_4} [] [] [] {a : M} {c : R} (hc : 0 < c) :
0 < a0 < c a

Alias of the reverse direction of smul_pos_iff_of_pos.

theorem monotone_smul_left {R : Type u_3} {M : Type u_4} [] [] [] {c : R} (hc : 0 c) :
theorem strictMono_smul_left {R : Type u_3} {M : Type u_4} [] [] [] {c : R} (hc : 0 < c) :
theorem smul_lowerBounds_subset_lowerBounds_smul {R : Type u_3} {M : Type u_4} [] [] [] {s : Set M} {c : R} (hc : 0 c) :
theorem smul_upperBounds_subset_upperBounds_smul {R : Type u_3} {M : Type u_4} [] [] [] {s : Set M} {c : R} (hc : 0 c) :
theorem BddBelow.smul_of_nonneg {R : Type u_3} {M : Type u_4} [] [] [] {s : Set M} {c : R} (hs : ) (hc : 0 c) :
theorem BddAbove.smul_of_nonneg {R : Type u_3} {M : Type u_4} [] [] [] {s : Set M} {c : R} (hs : ) (hc : 0 c) :
theorem OrderedSMul.mk'' {𝕜 : Type u_2} {M : Type u_4} [] [] (h : ∀ ⦃c : 𝕜⦄, 0 < cStrictMono fun a => c a) :

To prove that a linear ordered monoid is an ordered module, it suffices to verify only the first axiom of OrderedSMul.

instance Nat.orderedSMul {M : Type u_4} :
instance Int.orderedSMul {M : Type u_4} :
theorem OrderedSMul.mk' {𝕜 : Type u_2} {M : Type u_4} [] (h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b0 < cc a c b) :

To prove that a vector space over a linear ordered field is ordered, it suffices to verify only the first axiom of OrderedSMul.

instance Pi.orderedSMul {ι : Type u_1} {𝕜 : Type u_2} {M : ιType u_6} [(i : ι) → OrderedAddCommMonoid (M i)] [(i : ι) → MulActionWithZero 𝕜 (M i)] [∀ (i : ι), OrderedSMul 𝕜 (M i)] :
OrderedSMul 𝕜 ((i : ι) → M i)
instance Pi.orderedSMul' {ι : Type u_1} {𝕜 : Type u_2} {M : Type u_4} [] [] :
OrderedSMul 𝕜 (ιM)
instance Pi.orderedSMul'' {ι : Type u_1} {𝕜 : Type u_2} :
OrderedSMul 𝕜 (ι𝕜)
theorem smul_le_smul_iff_of_pos {𝕜 : Type u_2} {M : Type u_4} [] [] {a : M} {b : M} {c : 𝕜} (hc : 0 < c) :
c a c b a b
theorem inv_smul_le_iff {𝕜 : Type u_2} {M : Type u_4} [] [] {a : M} {b : M} {c : 𝕜} (h : 0 < c) :
c⁻¹ a b a c b
theorem inv_smul_lt_iff {𝕜 : Type u_2} {M : Type u_4} [] [] {a : M} {b : M} {c : 𝕜} (h : 0 < c) :
c⁻¹ a < b a < c b
theorem le_inv_smul_iff {𝕜 : Type u_2} {M : Type u_4} [] [] {a : M} {b : M} {c : 𝕜} (h : 0 < c) :
a c⁻¹ b c a b
theorem lt_inv_smul_iff {𝕜 : Type u_2} {M : Type u_4} [] [] {a : M} {b : M} {c : 𝕜} (h : 0 < c) :
a < c⁻¹ b c a < b
@[simp]
theorem OrderIso.smulLeft_symm_apply {𝕜 : Type u_2} (M : Type u_4) [] [] {c : 𝕜} (hc : 0 < c) (b : M) :
↑(RelIso.symm ()) b = c⁻¹ b
@[simp]
theorem OrderIso.smulLeft_apply {𝕜 : Type u_2} (M : Type u_4) [] [] {c : 𝕜} (hc : 0 < c) (b : M) :
↑() b = c b
def OrderIso.smulLeft {𝕜 : Type u_2} (M : Type u_4) [] [] {c : 𝕜} (hc : 0 < c) :
M ≃o M

Left scalar multiplication as an order isomorphism.

Instances For
@[simp]
theorem lowerBounds_smul_of_pos {𝕜 : Type u_2} {M : Type u_4} [] [] {s : Set M} {c : 𝕜} (hc : 0 < c) :
lowerBounds (c s) = c
@[simp]
theorem upperBounds_smul_of_pos {𝕜 : Type u_2} {M : Type u_4} [] [] {s : Set M} {c : 𝕜} (hc : 0 < c) :
upperBounds (c s) = c
@[simp]
theorem bddBelow_smul_iff_of_pos {𝕜 : Type u_2} {M : Type u_4} [] [] {s : Set M} {c : 𝕜} (hc : 0 < c) :
@[simp]
theorem bddAbove_smul_iff_of_pos {𝕜 : Type u_2} {M : Type u_4} [] [] {s : Set M} {c : 𝕜} (hc : 0 < c) :