# Documentation

Mathlib.Algebra.Order.Module

# Ordered module #

In this file we provide lemmas about OrderedSMul that hold once a module structure is present.

## References #

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

## Tags #

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

instance instModuleOrderDual {k : Type u_1} {M : Type u_2} [] [Module k M] :
theorem smul_neg_iff_of_pos {k : Type u_1} {M : Type u_2} [] [Module k M] [] {a : M} {c : k} (hc : 0 < c) :
c a < 0 a < 0
theorem smul_lt_smul_of_neg {k : Type u_1} {M : Type u_2} [] [Module k M] [] {a : M} {b : M} {c : k} (h : a < b) (hc : c < 0) :
c b < c a
theorem smul_le_smul_of_nonpos {k : Type u_1} {M : Type u_2} [] [Module k M] [] {a : M} {b : M} {c : k} (h : a b) (hc : c 0) :
c b c a
theorem eq_of_smul_eq_smul_of_neg_of_le {k : Type u_1} {M : Type u_2} [] [Module k M] [] {a : M} {b : M} {c : k} (hab : c a = c b) (hc : c < 0) (h : a b) :
a = b
theorem lt_of_smul_lt_smul_of_nonpos {k : Type u_1} {M : Type u_2} [] [Module k M] [] {a : M} {b : M} {c : k} (h : c a < c b) (hc : c 0) :
b < a
theorem smul_lt_smul_iff_of_neg {k : Type u_1} {M : Type u_2} [] [Module k M] [] {a : M} {b : M} {c : k} (hc : c < 0) :
c a < c b b < a
theorem smul_neg_iff_of_neg {k : Type u_1} {M : Type u_2} [] [Module k M] [] {a : M} {c : k} (hc : c < 0) :
c a < 0 0 < a
theorem smul_pos_iff_of_neg {k : Type u_1} {M : Type u_2} [] [Module k M] [] {a : M} {c : k} (hc : c < 0) :
0 < c a a < 0
theorem smul_nonpos_of_nonpos_of_nonneg {k : Type u_1} {M : Type u_2} [] [Module k M] [] {a : M} {c : k} (hc : c 0) (ha : 0 a) :
c a 0
theorem smul_nonneg_of_nonpos_of_nonpos {k : Type u_1} {M : Type u_2} [] [Module k M] [] {a : M} {c : k} (hc : c 0) (ha : a 0) :
0 c a
theorem smul_pos_of_neg_of_neg {k : Type u_1} {M : Type u_2} [] [Module k M] [] {a : M} {c : k} (hc : c < 0) :
a < 00 < c a

Alias of the reverse direction of smul_pos_iff_of_neg.

theorem smul_neg_of_pos_of_neg {k : Type u_1} {M : Type u_2} [] [Module k M] [] {a : M} {c : k} (hc : 0 < c) :
a < 0c a < 0

Alias of the reverse direction of smul_neg_iff_of_pos.

theorem smul_neg_of_neg_of_pos {k : Type u_1} {M : Type u_2} [] [Module k M] [] {a : M} {c : k} (hc : c < 0) :
0 < ac a < 0

Alias of the reverse direction of smul_neg_iff_of_neg.

theorem antitone_smul_left {k : Type u_1} {M : Type u_2} [] [Module k M] [] {c : k} (hc : c 0) :
theorem strict_anti_smul_left {k : Type u_1} {M : Type u_2} [] [Module k M] [] {c : k} (hc : c < 0) :
theorem smul_add_smul_le_smul_add_smul {k : Type u_1} {M : Type u_2} [] [Module k M] [] [ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : k} {b : k} {c : M} {d : M} (hab : a b) (hcd : c d) :
a d + b c a c + b d

Binary rearrangement inequality.

theorem smul_add_smul_le_smul_add_smul' {k : Type u_1} {M : Type u_2} [] [Module k M] [] [ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : k} {b : k} {c : M} {d : M} (hba : b a) (hdc : d c) :
a d + b c a c + b d

Binary rearrangement inequality.

theorem smul_add_smul_lt_smul_add_smul {k : Type u_1} {M : Type u_2} [] [Module k M] [] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : k} {b : k} {c : M} {d : M} (hab : a < b) (hcd : c < d) :
a d + b c < a c + b d

Binary strict rearrangement inequality.

theorem smul_add_smul_lt_smul_add_smul' {k : Type u_1} {M : Type u_2} [] [Module k M] [] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : k} {b : k} {c : M} {d : M} (hba : b < a) (hdc : d < c) :
a d + b c < a c + b d

Binary strict rearrangement inequality.

theorem smul_le_smul_iff_of_neg {k : Type u_1} {M : Type u_2} [Module k M] [] {a : M} {b : M} {c : k} (hc : c < 0) :
c a c b b a
theorem inv_smul_le_iff_of_neg {k : Type u_1} {M : Type u_2} [Module k M] [] {a : M} {b : M} {c : k} (h : c < 0) :
c⁻¹ a b c b a
theorem inv_smul_lt_iff_of_neg {k : Type u_1} {M : Type u_2} [Module k M] [] {a : M} {b : M} {c : k} (h : c < 0) :
c⁻¹ a < b c b < a
theorem smul_inv_le_iff_of_neg {k : Type u_1} {M : Type u_2} [Module k M] [] {a : M} {b : M} {c : k} (h : c < 0) :
a c⁻¹ b b c a
theorem smul_inv_lt_iff_of_neg {k : Type u_1} {M : Type u_2} [Module k M] [] {a : M} {b : M} {c : k} (h : c < 0) :
a < c⁻¹ b b < c a
@[simp]
theorem OrderIso.smulLeftDual_symm_apply {k : Type u_1} (M : Type u_2) [Module k M] [] {c : k} (hc : c < 0) (b : Mᵒᵈ) :
↑() b = c⁻¹ OrderDual.ofDual b
@[simp]
theorem OrderIso.smulLeftDual_apply {k : Type u_1} (M : Type u_2) [Module k M] [] {c : k} (hc : c < 0) (b : M) :
↑() b = OrderDual.toDual (c b)
def OrderIso.smulLeftDual {k : Type u_1} (M : Type u_2) [Module k M] [] {c : k} (hc : c < 0) :

Left scalar multiplication as an order isomorphism.

Instances For

### Upper/lower bounds #

theorem smul_lowerBounds_subset_upperBounds_smul {k : Type u_1} {M : Type u_2} [] [Module k M] [] {s : Set M} {c : k} (hc : c 0) :
theorem smul_upperBounds_subset_lowerBounds_smul {k : Type u_1} {M : Type u_2} [] [Module k M] [] {s : Set M} {c : k} (hc : c 0) :
theorem BddBelow.smul_of_nonpos {k : Type u_1} {M : Type u_2} [] [Module k M] [] {s : Set M} {c : k} (hc : c 0) (hs : ) :
theorem BddAbove.smul_of_nonpos {k : Type u_1} {M : Type u_2} [] [Module k M] [] {s : Set M} {c : k} (hc : c 0) (hs : ) :
@[simp]
theorem lowerBounds_smul_of_neg {k : Type u_1} {M : Type u_2} [Module k M] [] {s : Set M} {c : k} (hc : c < 0) :
lowerBounds (c s) = c
@[simp]
theorem upperBounds_smul_of_neg {k : Type u_1} {M : Type u_2} [Module k M] [] {s : Set M} {c : k} (hc : c < 0) :
upperBounds (c s) = c
@[simp]
theorem bddBelow_smul_iff_of_neg {k : Type u_1} {M : Type u_2} [Module k M] [] {s : Set M} {c : k} (hc : c < 0) :
@[simp]
theorem bddAbove_smul_iff_of_neg {k : Type u_1} {M : Type u_2} [Module k M] [] {s : Set M} {c : k} (hc : c < 0) :