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
@[instance]
def order_dual.has_scalar {R : Type u_1} {M : Type u_2} [has_scalar R M] :
Equations
@[instance]
def order_dual.mul_action {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] :
Equations
@[instance]
@[simp]
theorem order_dual.to_dual_smul {R : Type u_1} {M : Type u_2} [has_scalar R M] {c : R} {a : M} :
@[simp]
theorem order_dual.of_dual_smul {R : Type u_1} {M : Type u_2} [has_scalar R M] {c : R} {a : order_dual M} :
theorem smul_lt_smul_of_pos {R : Type u_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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 smul_pos_iff_of_pos.

theorem monotone_smul_left {R : Type u_1} {M : Type u_2} [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_1} {M : Type u_2} [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M] [ordered_smul R M] {c : R} (hc : 0 < c) :
theorem ordered_smul.mk'' {R : Type u_1} {M : Type u_2} [linear_ordered_semiring R] [ordered_add_comm_monoid M] [mul_action_with_zero R M] (hR : ∀ {c : R}, c 0is_unit c) (hlt : ∀ ⦃a b : M⦄ ⦃c : R⦄, a < b0 < cc a c b) :

If R is a linear ordered semifield, then it suffices to verify only the first axiom of ordered_smul. Moreover, it suffices to verify that a < b and 0 < c imply c • a ≤ c • b. We have no semifields in mathlib, so we use the assumption ∀ c ≠ 0, is_unit c instead.

theorem ordered_smul.mk' {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_monoid M] [mul_action_with_zero k M] (hlt : ∀ ⦃a b : M⦄ ⦃c : k⦄, a < b0 < cc a c b) :

If R is a linear ordered field, then it suffices to verify only the first axiom of ordered_smul.

theorem smul_le_smul_iff_of_pos {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_group M] [mul_action_with_zero k M] [ordered_smul k M] {a b : M} {c : k} (hc : 0 < c) :
c a c b a b
theorem smul_lt_iff_of_pos {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_group M] [mul_action_with_zero k M] [ordered_smul k M] {a b : M} {c : k} (hc : 0 < c) :
c a < b a < c⁻¹ b
theorem lt_smul_iff_of_pos {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_group M] [mul_action_with_zero k M] [ordered_smul k M] {a b : M} {c : k} (hc : 0 < c) :
a < c b c⁻¹ a < b
theorem smul_le_iff_of_pos {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_group M] [mul_action_with_zero k M] [ordered_smul k M] {a b : M} {c : k} (hc : 0 < c) :
c a b a c⁻¹ b
theorem le_smul_iff_of_pos {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_group M] [mul_action_with_zero k M] [ordered_smul k M] {a b : M} {c : k} (hc : 0 < c) :
a c b c⁻¹ a b
@[simp]
theorem order_iso.smul_left_apply {k : Type u_1} (M : Type u_2) [linear_ordered_field k] [ordered_add_comm_group M] [mul_action_with_zero k M] [ordered_smul k M] {c : k} (hc : 0 < c) (b : M) :
def order_iso.smul_left {k : Type u_1} (M : Type u_2) [linear_ordered_field k] [ordered_add_comm_group M] [mul_action_with_zero k M] [ordered_smul k M] {c : k} (hc : 0 < c) :
M ≃o M

Left scalar multiplication as an order isomorphism.

Equations
@[simp]
theorem order_iso.smul_left_symm_apply {k : Type u_1} (M : Type u_2) [linear_ordered_field k] [ordered_add_comm_group M] [mul_action_with_zero k M] [ordered_smul k M] {c : k} (hc : 0 < c) (b : M) :