mathlib documentation

algebra.order.smul

Ordered scalar product #

In this file we define

Implementation notes #

References #

Tags #

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

@[class]
structure ordered_smul (R : Type u_1) (M : Type u_2) [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M] :
Prop
  • smul_lt_smul_of_pos : ∀ {a b : M} {c : R}, a < b0 < cc a < c b
  • lt_of_smul_lt_smul_of_pos : ∀ {a b : M} {c : R}, c a < c b0 < ca < 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 of this typeclass
@[protected, instance]
def order_dual.mul_action {R : Type u_3} {M : Type u_4} [monoid R] [mul_action R M] :
Equations
@[protected, instance]
theorem smul_lt_smul_of_pos {R : Type u_3} {M : Type u_4} [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M] [ordered_smul R M] {a b : M} {c : R} :
a < b0 < cc a < c b
theorem smul_le_smul_of_nonneg {R : Type u_3} {M : Type u_4} [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M] [ordered_smul R M] {a 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} [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M] [ordered_smul R M] {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} [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M] [ordered_smul R M] {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} [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M] [ordered_smul R M] {a 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} [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M] [ordered_smul R M] {a 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} [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M] [ordered_smul R M] {a 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} [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M] [ordered_smul R M] {a : M} {c : R} (hc : 0 < c) :
0 < c a 0 < a
theorem smul_pos {R : Type u_3} {M : Type u_4} [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M] [ordered_smul R M] {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} [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M] [ordered_smul R M] {c : R} (hc : 0 c) :
theorem strict_mono_smul_left {R : Type u_3} {M : Type u_4} [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M] [ordered_smul R M] {c : R} (hc : 0 < c) :
theorem smul_lower_bounds_subset_lower_bounds_smul {R : Type u_3} {M : Type u_4} [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M] [ordered_smul R M] {s : set M} {c : R} (hc : 0 c) :
theorem smul_upper_bounds_subset_upper_bounds_smul {R : Type u_3} {M : Type u_4} [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M] [ordered_smul R M] {s : set M} {c : R} (hc : 0 c) :
theorem bdd_below.smul_of_nonneg {R : Type u_3} {M : Type u_4} [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M] [ordered_smul R M] {s : set M} {c : R} (hs : bdd_below s) (hc : 0 c) :
theorem bdd_above.smul_of_nonneg {R : Type u_3} {M : Type u_4} [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M] [ordered_smul R M] {s : set M} {c : R} (hs : bdd_above s) (hc : 0 c) :
theorem ordered_smul.mk'' {𝕜 : Type u_2} {M : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid M] [smul_with_zero 𝕜 M] (h : ∀ ⦃c : 𝕜⦄, 0 < cstrict_mono (λ (a : M), c a)) :

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

@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem ordered_smul.mk' {𝕜 : Type u_2} {M : Type u_4} [linear_ordered_semifield 𝕜] [ordered_add_comm_monoid M] [mul_action_with_zero 𝕜 M] (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 ordered_smul.

@[protected, instance]
def prod.ordered_smul {𝕜 : Type u_2} {M : Type u_4} {N : Type u_5} [linear_ordered_semifield 𝕜] [ordered_add_comm_monoid M] [ordered_add_comm_monoid N] [mul_action_with_zero 𝕜 M] [mul_action_with_zero 𝕜 N] [ordered_smul 𝕜 M] [ordered_smul 𝕜 N] :
ordered_smul 𝕜 (M × N)
@[protected, instance]
def pi.ordered_smul {ι : Type u_1} {𝕜 : Type u_2} [linear_ordered_semifield 𝕜] {M : ι → Type u_3} [Π (i : ι), ordered_add_comm_monoid (M i)] [Π (i : ι), mul_action_with_zero 𝕜 (M i)] [∀ (i : ι), ordered_smul 𝕜 (M i)] :
ordered_smul 𝕜 (Π (i : ι), M i)
@[protected, instance]
def pi.ordered_smul' {ι : Type u_1} {𝕜 : Type u_2} {M : Type u_4} [linear_ordered_semifield 𝕜] [ordered_add_comm_monoid M] [mul_action_with_zero 𝕜 M] [ordered_smul 𝕜 M] :
ordered_smul 𝕜 (ι → M)
@[protected, instance]
def pi.ordered_smul'' {ι : Type u_1} {𝕜 : Type u_2} [linear_ordered_semifield 𝕜] :
ordered_smul 𝕜 (ι → 𝕜)
theorem smul_le_smul_iff_of_pos {𝕜 : Type u_2} {M : Type u_4} [linear_ordered_semifield 𝕜] [ordered_add_comm_group M] [mul_action_with_zero 𝕜 M] [ordered_smul 𝕜 M] {a b : M} {c : 𝕜} (hc : 0 < c) :
c a c b a b
theorem smul_lt_iff_of_pos {𝕜 : Type u_2} {M : Type u_4} [linear_ordered_semifield 𝕜] [ordered_add_comm_group M] [mul_action_with_zero 𝕜 M] [ordered_smul 𝕜 M] {a b : M} {c : 𝕜} (hc : 0 < c) :
c a < b a < c⁻¹ b
theorem lt_smul_iff_of_pos {𝕜 : Type u_2} {M : Type u_4} [linear_ordered_semifield 𝕜] [ordered_add_comm_group M] [mul_action_with_zero 𝕜 M] [ordered_smul 𝕜 M] {a b : M} {c : 𝕜} (hc : 0 < c) :
a < c b c⁻¹ a < b
theorem smul_le_iff_of_pos {𝕜 : Type u_2} {M : Type u_4} [linear_ordered_semifield 𝕜] [ordered_add_comm_group M] [mul_action_with_zero 𝕜 M] [ordered_smul 𝕜 M] {a b : M} {c : 𝕜} (hc : 0 < c) :
c a b a c⁻¹ b
theorem le_smul_iff_of_pos {𝕜 : Type u_2} {M : Type u_4} [linear_ordered_semifield 𝕜] [ordered_add_comm_group M] [mul_action_with_zero 𝕜 M] [ordered_smul 𝕜 M] {a b : M} {c : 𝕜} (hc : 0 < c) :
a c b c⁻¹ a b
@[simp]
theorem order_iso.smul_left_apply {𝕜 : Type u_2} (M : Type u_4) [linear_ordered_semifield 𝕜] [ordered_add_comm_group M] [mul_action_with_zero 𝕜 M] [ordered_smul 𝕜 M] {c : 𝕜} (hc : 0 < c) (b : M) :
def order_iso.smul_left {𝕜 : Type u_2} (M : Type u_4) [linear_ordered_semifield 𝕜] [ordered_add_comm_group M] [mul_action_with_zero 𝕜 M] [ordered_smul 𝕜 M] {c : 𝕜} (hc : 0 < c) :
M ≃o M

Left scalar multiplication as an order isomorphism.

Equations
@[simp]
theorem order_iso.smul_left_symm_apply {𝕜 : Type u_2} (M : Type u_4) [linear_ordered_semifield 𝕜] [ordered_add_comm_group M] [mul_action_with_zero 𝕜 M] [ordered_smul 𝕜 M] {c : 𝕜} (hc : 0 < c) (b : M) :
@[simp]
theorem lower_bounds_smul_of_pos {𝕜 : Type u_2} {M : Type u_4} [linear_ordered_semifield 𝕜] [ordered_add_comm_group M] [mul_action_with_zero 𝕜 M] [ordered_smul 𝕜 M] {s : set M} {c : 𝕜} (hc : 0 < c) :
@[simp]
theorem upper_bounds_smul_of_pos {𝕜 : Type u_2} {M : Type u_4} [linear_ordered_semifield 𝕜] [ordered_add_comm_group M] [mul_action_with_zero 𝕜 M] [ordered_smul 𝕜 M] {s : set M} {c : 𝕜} (hc : 0 < c) :
@[simp]
theorem bdd_below_smul_iff_of_pos {𝕜 : Type u_2} {M : Type u_4} [linear_ordered_semifield 𝕜] [ordered_add_comm_group M] [mul_action_with_zero 𝕜 M] [ordered_smul 𝕜 M] {s : set M} {c : 𝕜} (hc : 0 < c) :
@[simp]
theorem bdd_above_smul_iff_of_pos {𝕜 : Type u_2} {M : Type u_4} [linear_ordered_semifield 𝕜] [ordered_add_comm_group M] [mul_action_with_zero 𝕜 M] [ordered_smul 𝕜 M] {s : set M} {c : 𝕜} (hc : 0 < c) :

Extension for the positivity tactic: scalar multiplication is nonnegative if both sides are nonnegative, and strictly positive if both sides are.