# Monotonicity of scalar multiplication by positive elements #

This file defines typeclasses to reason about monotonicity of the operations

• b ↦ a • b, "left scalar multiplication"
• a ↦ a • b, "right scalar multiplication"

We use eight typeclasses to encode the various properties we care about for those two operations. These typeclasses are meant to be mostly internal to this file, to set up each lemma in the appropriate generality.

Less granular typeclasses like OrderedAddCommMonoid, LinearOrderedField, OrderedSMul should be enough for most purposes, and the system is set up so that they imply the correct granular typeclasses here. If those are enough for you, you may stop reading here! Else, beware that what follows is a bit technical.

## Definitions #

In all that follows, α and β are orders which have a 0 and such that α acts on β by scalar multiplication. Note however that we do not use lawfulness of this action in most of the file. Hence should be considered here as a mostly arbitrary function α → β → β.

We use the following four typeclasses to reason about left scalar multiplication (b ↦ a • b):

• PosSMulMono: If a ≥ 0, then b₁ ≤ b₂ implies a • b₁ ≤ a • b₂.
• PosSMulStrictMono: If a > 0, then b₁ < b₂ implies a • b₁ < a • b₂.
• PosSMulReflectLT: If a ≥ 0, then a • b₁ < a • b₂ implies b₁ < b₂.
• PosSMulReflectLE: If a > 0, then a • b₁ ≤ a • b₂ implies b₁ ≤ b₂.

We use the following four typeclasses to reason about right scalar multiplication (a ↦ a • b):

• SMulPosMono: If b ≥ 0, then a₁ ≤ a₂ implies a₁ • b ≤ a₂ • b.
• SMulPosStrictMono: If b > 0, then a₁ < a₂ implies a₁ • b < a₂ • b.
• SMulPosReflectLT: If b ≥ 0, then a₁ • b < a₂ • b implies a₁ < a₂.
• SMulPosReflectLE: If b > 0, then a₁ • b ≤ a₂ • b implies a₁ ≤ a₂.

## Constructors #

The four typeclasses about nonnegativity can usually be checked only on positive inputs due to their condition becoming trivial when a = 0 or b = 0. We therefore make the following constructors available: PosSMulMono.of_pos, PosSMulReflectLT.of_pos, SMulPosMono.of_pos, SMulPosReflectLT.of_pos

## Implications #

As α and β get more and more structure, those typeclasses end up being equivalent. The commonly used implications are:

Further, the bundled non-granular typeclasses imply the granular ones like so:

All these are registered as instances, which means that in practice you should not worry about these implications. However, if you encounter a case where you think a statement is true but not covered by the current implications, please bring it up on Zulip!

## Implementation notes #

This file uses custom typeclasses instead of abbreviations of CovariantClass/ContravariantClass because:

• They get displayed as classes in the docs. In particular, one can see their list of instances, instead of their instances being invariably dumped to the CovariantClass/ContravariantClass list.
• They don't pollute other typeclass searches. Having many abbreviations of the same typeclass for different purposes always felt like a performance issue (more instances with the same key, for no added benefit), and indeed making the classes here abbreviation previous creates timeouts due to the higher number of CovariantClass/ContravariantClass instances.
• SMulPosReflectLT/SMulPosReflectLE do not fit in the framework since they relate on two different types. So we would have to generalise CovariantClass/ContravariantClass to three types and two relations.
• Very minor, but the constructors let you work with a : α, h : 0 ≤ a instead of a : {a : α // 0 ≤ a}. This actually makes some instances surprisingly cleaner to prove.
• The CovariantClass/ContravariantClass framework is only useful to automate very simple logic anyway. It is easily copied over.

In the future, it would be good to make the corresponding typeclasses in Mathlib.Algebra.Order.Ring.Lemmas custom typeclasses too.

## TODO #

This file acts as a substitute for Mathlib.Algebra.Order.SMul. We now need to

• finish the transition by deleting the duplicate lemmas
• rearrange the non-duplicate lemmas into new files
• generalise (most of) the lemmas from Mathlib.Algebra.Order.Module to here
• rethink OrderedSMul
class PosSMulMono (α : Type u_1) (β : Type u_2) [SMul α β] [] [] [Zero α] :

Typeclass for monotonicity of scalar multiplication by nonnegative elements on the left, namely b₁ ≤ b₂ → a • b₁ ≤ a • b₂ if 0 ≤ a.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedSMul.

Instances
theorem PosSMulMono.elim {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero α] [self : ] ⦃a : α (ha : 0 a) ⦃b₁ : β ⦃b₂ : β (hb : b₁ b₂) :
a b₁ a b₂

Do not use this. Use smul_le_smul_of_nonneg_left instead.

class PosSMulStrictMono (α : Type u_1) (β : Type u_2) [SMul α β] [] [] [Zero α] :

Typeclass for strict monotonicity of scalar multiplication by positive elements on the left, namely b₁ < b₂ → a • b₁ < a • b₂ if 0 < a.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedSMul.

Instances
theorem PosSMulStrictMono.elim {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero α] [self : ] ⦃a : α (ha : 0 < a) ⦃b₁ : β ⦃b₂ : β (hb : b₁ < b₂) :
a b₁ < a b₂

Do not use this. Use smul_lt_smul_of_pos_left instead.

class PosSMulReflectLT (α : Type u_1) (β : Type u_2) [SMul α β] [] [] [Zero α] :

Typeclass for strict reverse monotonicity of scalar multiplication by nonnegative elements on the left, namely a • b₁ < a • b₂ → b₁ < b₂ if 0 ≤ a.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedSMul.

Instances
theorem PosSMulReflectLT.elim {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero α] [self : ] ⦃a : α (ha : 0 a) ⦃b₁ : β ⦃b₂ : β (hb : a b₁ < a b₂) :
b₁ < b₂

Do not use this. Use lt_of_smul_lt_smul_left instead.

class PosSMulReflectLE (α : Type u_1) (β : Type u_2) [SMul α β] [] [] [Zero α] :

Typeclass for reverse monotonicity of scalar multiplication by positive elements on the left, namely a • b₁ ≤ a • b₂ → b₁ ≤ b₂ if 0 < a.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedSMul.

• elim : ∀ ⦃a : α⦄, 0 < a∀ ⦃b₁ b₂ : β⦄, a b₁ a b₂b₁ b₂

Do not use this. Use le_of_smul_lt_smul_left instead.

Instances
theorem PosSMulReflectLE.elim {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero α] [self : ] ⦃a : α (ha : 0 < a) ⦃b₁ : β ⦃b₂ : β (hb : a b₁ a b₂) :
b₁ b₂

Do not use this. Use le_of_smul_lt_smul_left instead.

class SMulPosMono (α : Type u_1) (β : Type u_2) [SMul α β] [] [] [Zero β] :

Typeclass for monotonicity of scalar multiplication by nonnegative elements on the left, namely a₁ ≤ a₂ → a₁ • b ≤ a₂ • b if 0 ≤ b.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedSMul.

Instances
theorem SMulPosMono.elim {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero β] [self : ] ⦃b : β (hb : 0 b) ⦃a₁ : α ⦃a₂ : α (ha : a₁ a₂) :
a₁ b a₂ b

Do not use this. Use smul_le_smul_of_nonneg_right instead.

class SMulPosStrictMono (α : Type u_1) (β : Type u_2) [SMul α β] [] [] [Zero β] :

Typeclass for strict monotonicity of scalar multiplication by positive elements on the left, namely a₁ < a₂ → a₁ • b < a₂ • b if 0 < b.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedSMul.

Instances
theorem SMulPosStrictMono.elim {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero β] [self : ] ⦃b : β (hb : 0 < b) ⦃a₁ : α ⦃a₂ : α (ha : a₁ < a₂) :
a₁ b < a₂ b

Do not use this. Use smul_lt_smul_of_pos_right instead.

class SMulPosReflectLT (α : Type u_1) (β : Type u_2) [SMul α β] [] [] [Zero β] :

Typeclass for strict reverse monotonicity of scalar multiplication by nonnegative elements on the left, namely a₁ • b < a₂ • b → a₁ < a₂ if 0 ≤ b.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedSMul.

Instances
theorem SMulPosReflectLT.elim {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero β] [self : ] ⦃b : β (hb : 0 b) ⦃a₁ : α ⦃a₂ : α (hb : a₁ b < a₂ b) :
a₁ < a₂

Do not use this. Use lt_of_smul_lt_smul_right instead.

class SMulPosReflectLE (α : Type u_1) (β : Type u_2) [SMul α β] [] [] [Zero β] :

Typeclass for reverse monotonicity of scalar multiplication by positive elements on the left, namely a₁ • b ≤ a₂ • b → a₁ ≤ a₂ if 0 < b.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedSMul.

• elim : ∀ ⦃b : β⦄, 0 < b∀ ⦃a₁ a₂ : α⦄, a₁ b a₂ ba₁ a₂

Do not use this. Use le_of_smul_lt_smul_right instead.

Instances
theorem SMulPosReflectLE.elim {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero β] [self : ] ⦃b : β (hb : 0 < b) ⦃a₁ : α ⦃a₂ : α (hb : a₁ b a₂ b) :
a₁ a₂

Do not use this. Use le_of_smul_lt_smul_right instead.

@[instance 100]
instance PosMulMono.toPosSMulMono {α : Type u_1} [Zero α] [Mul α] [] [] :
Equations
• =
@[instance 100]
instance PosMulStrictMono.toPosSMulStrictMono {α : Type u_1} [Zero α] [Mul α] [] [] :
Equations
• =
@[instance 100]
instance PosMulReflectLT.toPosSMulReflectLT {α : Type u_1} [Zero α] [Mul α] [] [] :
Equations
• =
@[instance 100]
instance PosMulReflectLE.toPosSMulReflectLE {α : Type u_1} [Zero α] [Mul α] [] [] :
Equations
• =
@[instance 100]
instance MulPosMono.toSMulPosMono {α : Type u_1} [Zero α] [Mul α] [] [] :
Equations
• =
@[instance 100]
instance MulPosStrictMono.toSMulPosStrictMono {α : Type u_1} [Zero α] [Mul α] [] [] :
Equations
• =
@[instance 100]
instance MulPosReflectLT.toSMulPosReflectLT {α : Type u_1} [Zero α] [Mul α] [] [] :
Equations
• =
@[instance 100]
instance MulPosReflectLE.toSMulPosReflectLE {α : Type u_1} [Zero α] [Mul α] [] [] :
Equations
• =
theorem monotone_smul_left_of_nonneg {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [] [] [Zero α] [] (ha : 0 a) :
Monotone fun (x : β) => a x
theorem strictMono_smul_left_of_pos {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [] [] [Zero α] [] (ha : 0 < a) :
StrictMono fun (x : β) => a x
theorem smul_le_smul_of_nonneg_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [] [] [Zero α] [] (hb : b₁ b₂) (ha : 0 a) :
a b₁ a b₂
theorem smul_lt_smul_of_pos_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [] [] [Zero α] [] (hb : b₁ < b₂) (ha : 0 < a) :
a b₁ < a b₂
theorem lt_of_smul_lt_smul_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [] [] [Zero α] [] (h : a b₁ < a b₂) (ha : 0 a) :
b₁ < b₂
theorem le_of_smul_le_smul_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [] [] [Zero α] [] (h : a b₁ a b₂) (ha : 0 < a) :
b₁ b₂
theorem lt_of_smul_lt_smul_of_nonneg_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [] [] [Zero α] [] (h : a b₁ < a b₂) (ha : 0 a) :
b₁ < b₂

Alias of lt_of_smul_lt_smul_left.

theorem le_of_smul_le_smul_of_pos_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [] [] [Zero α] [] (h : a b₁ a b₂) (ha : 0 < a) :
b₁ b₂

Alias of le_of_smul_le_smul_left.

@[simp]
theorem smul_le_smul_iff_of_pos_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [] [] [Zero α] [] [] (ha : 0 < a) :
a b₁ a b₂ b₁ b₂
@[simp]
theorem smul_lt_smul_iff_of_pos_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [] [] [Zero α] [] [] (ha : 0 < a) :
a b₁ < a b₂ b₁ < b₂
theorem monotone_smul_right_of_nonneg {α : Type u_1} {β : Type u_2} {b : β} [SMul α β] [] [] [Zero β] [] (hb : 0 b) :
Monotone fun (x : α) => x b
theorem strictMono_smul_right_of_pos {α : Type u_1} {β : Type u_2} {b : β} [SMul α β] [] [] [Zero β] [] (hb : 0 < b) :
StrictMono fun (x : α) => x b
theorem smul_le_smul_of_nonneg_right {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b : β} [SMul α β] [] [] [Zero β] [] (ha : a₁ a₂) (hb : 0 b) :
a₁ b a₂ b
theorem smul_lt_smul_of_pos_right {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b : β} [SMul α β] [] [] [Zero β] [] (ha : a₁ < a₂) (hb : 0 < b) :
a₁ b < a₂ b
theorem lt_of_smul_lt_smul_right {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b : β} [SMul α β] [] [] [Zero β] [] (h : a₁ b < a₂ b) (hb : 0 b) :
a₁ < a₂
theorem le_of_smul_le_smul_right {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b : β} [SMul α β] [] [] [Zero β] [] (h : a₁ b a₂ b) (hb : 0 < b) :
a₁ a₂
theorem lt_of_smul_lt_smul_of_nonneg_right {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b : β} [SMul α β] [] [] [Zero β] [] (h : a₁ b < a₂ b) (hb : 0 b) :
a₁ < a₂

Alias of lt_of_smul_lt_smul_right.

theorem le_of_smul_le_smul_of_pos_right {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b : β} [SMul α β] [] [] [Zero β] [] (h : a₁ b a₂ b) (hb : 0 < b) :
a₁ a₂

Alias of le_of_smul_le_smul_right.

@[simp]
theorem smul_le_smul_iff_of_pos_right {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b : β} [SMul α β] [] [] [Zero β] [] [] (hb : 0 < b) :
a₁ b a₂ b a₁ a₂
@[simp]
theorem smul_lt_smul_iff_of_pos_right {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b : β} [SMul α β] [] [] [Zero β] [] [] (hb : 0 < b) :
a₁ b < a₂ b a₁ < a₂
theorem smul_lt_smul_of_le_of_lt {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} [SMul α β] [] [] [Zero α] [Zero β] [] [] (ha : a₁ a₂) (hb : b₁ < b₂) (h₁ : 0 < a₁) (h₂ : 0 b₂) :
a₁ b₁ < a₂ b₂
theorem smul_lt_smul_of_le_of_lt' {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} [SMul α β] [] [] [Zero α] [Zero β] [] [] (ha : a₁ a₂) (hb : b₁ < b₂) (h₂ : 0 < a₂) (h₁ : 0 b₁) :
a₁ b₁ < a₂ b₂
theorem smul_lt_smul_of_lt_of_le {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} [SMul α β] [] [] [Zero α] [Zero β] [] [] (ha : a₁ < a₂) (hb : b₁ b₂) (h₁ : 0 a₁) (h₂ : 0 < b₂) :
a₁ b₁ < a₂ b₂
theorem smul_lt_smul_of_lt_of_le' {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} [SMul α β] [] [] [Zero α] [Zero β] [] [] (ha : a₁ < a₂) (hb : b₁ b₂) (h₂ : 0 a₂) (h₁ : 0 < b₁) :
a₁ b₁ < a₂ b₂
theorem smul_lt_smul {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} [SMul α β] [] [] [Zero α] [Zero β] [] [] (ha : a₁ < a₂) (hb : b₁ < b₂) (h₁ : 0 < a₁) (h₂ : 0 < b₂) :
a₁ b₁ < a₂ b₂
theorem smul_lt_smul' {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} [SMul α β] [] [] [Zero α] [Zero β] [] [] (ha : a₁ < a₂) (hb : b₁ < b₂) (h₂ : 0 < a₂) (h₁ : 0 < b₁) :
a₁ b₁ < a₂ b₂
theorem smul_le_smul {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} [SMul α β] [] [] [Zero α] [Zero β] [] [] (ha : a₁ a₂) (hb : b₁ b₂) (h₁ : 0 a₁) (h₂ : 0 b₂) :
a₁ b₁ a₂ b₂
theorem smul_le_smul' {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} [SMul α β] [] [] [Zero α] [Zero β] [] [] (ha : a₁ a₂) (hb : b₁ b₂) (h₂ : 0 a₂) (h₁ : 0 b₁) :
a₁ b₁ a₂ b₂
@[instance 100]
instance PosSMulStrictMono.toPosSMulReflectLE {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero α] [] :
Equations
• =
theorem PosSMulReflectLE.toPosSMulStrictMono {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero α] [] :
theorem posSMulStrictMono_iff_PosSMulReflectLE {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero α] :
instance PosSMulMono.toPosSMulReflectLT {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero α] [] :
Equations
• =
theorem PosSMulReflectLT.toPosSMulMono {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero α] [] :
theorem posSMulMono_iff_posSMulReflectLT {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero α] :
theorem smul_max_of_nonneg {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [] [] [Zero α] [] (ha : 0 a) (b₁ : β) (b₂ : β) :
a max b₁ b₂ = max (a b₁) (a b₂)
theorem smul_min_of_nonneg {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [] [] [Zero α] [] (ha : 0 a) (b₁ : β) (b₂ : β) :
a min b₁ b₂ = min (a b₁) (a b₂)
theorem SMulPosReflectLE.toSMulPosStrictMono {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero β] [] :
theorem SMulPosReflectLT.toSMulPosMono {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero β] [] :
@[instance 100]
instance SMulPosStrictMono.toSMulPosReflectLE {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero β] [] :
Equations
• =
theorem SMulPosMono.toSMulPosReflectLT {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero β] [] :
theorem smulPosStrictMono_iff_SMulPosReflectLE {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero β] :
theorem smulPosMono_iff_smulPosReflectLT {α : Type u_1} {β : Type u_2} [SMul α β] [] [] [Zero β] :
theorem smul_pos {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] (ha : 0 < a) (hb : 0 < b) :
0 < a b
theorem smul_neg_of_pos_of_neg {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] (ha : 0 < a) (hb : b < 0) :
a b < 0
@[simp]
theorem smul_pos_iff_of_pos_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] [] (ha : 0 < a) :
0 < a b 0 < b
theorem smul_neg_iff_of_pos_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] [] (ha : 0 < a) :
a b < 0 b < 0
theorem smul_nonneg {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} [Zero α] [Zero β] [] [] [] [] (ha : 0 a) (hb : 0 b₁) :
0 a b₁
theorem smul_nonpos_of_nonneg_of_nonpos {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] (ha : 0 a) (hb : b 0) :
a b 0
theorem pos_of_smul_pos_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] (h : 0 < a b) (ha : 0 a) :
0 < b
theorem neg_of_smul_neg_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] (h : a b < 0) (ha : 0 a) :
b < 0
theorem smul_pos' {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] (ha : 0 < a) (hb : 0 < b) :
0 < a b
theorem smul_neg_of_neg_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] (ha : a < 0) (hb : 0 < b) :
a b < 0
@[simp]
theorem smul_pos_iff_of_pos_right {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] [] (hb : 0 < b) :
0 < a b 0 < a
theorem smul_nonneg' {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} [Zero α] [Zero β] [] [] [] [] (ha : 0 a) (hb : 0 b₁) :
0 a b₁
theorem smul_nonpos_of_nonpos_of_nonneg {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] (ha : a 0) (hb : 0 b) :
a b 0
theorem pos_of_smul_pos_right {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] (h : 0 < a b) (hb : 0 b) :
0 < a
theorem neg_of_smul_neg_right {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] (h : a b < 0) (hb : 0 b) :
a < 0
theorem pos_iff_pos_of_smul_pos {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] [] (hab : 0 < a b) :
0 < a 0 < b
theorem PosSMulMono.of_pos {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [] [] [] (h₀ : ∀ (a : α), 0 < a∀ (b₁ b₂ : β), b₁ b₂a b₁ a b₂) :

A constructor for PosSMulMono requiring you to prove b₁ ≤ b₂ → a • b₁ ≤ a • b₂ only when 0 < a

theorem PosSMulReflectLT.of_pos {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [] [] [] (h₀ : ∀ (a : α), 0 < a∀ (b₁ b₂ : β), a b₁ < a b₂b₁ < b₂) :

A constructor for PosSMulReflectLT requiring you to prove a • b₁ < a • b₂ → b₁ < b₂ only when 0 < a

theorem SMulPosMono.of_pos {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [] [] [] (h₀ : ∀ (b : β), 0 < b∀ (a₁ a₂ : α), a₁ a₂a₁ b a₂ b) :

A constructor for SMulPosMono requiring you to prove a₁ ≤ a₂ → a₁ • b ≤ a₂ • b only when 0 < b

theorem SMulPosReflectLT.of_pos {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [] [] [] (h₀ : ∀ (b : β), 0 < b∀ (a₁ a₂ : α), a₁ b < a₂ ba₁ < a₂) :

A constructor for SMulPosReflectLT requiring you to prove a₁ • b < a₂ • b → a₁ < a₂ only when 0 < b

@[instance 100]
instance PosSMulStrictMono.toPosSMulMono {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [] [] [] [] :
Equations
• =
@[instance 100]
instance SMulPosStrictMono.toSMulPosMono {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [] [] [] [] :
Equations
• =
@[instance 100]
instance PosSMulReflectLE.toPosSMulReflectLT {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [] [] [] [] :
Equations
• =
@[instance 100]
instance SMulPosReflectLE.toSMulPosReflectLT {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [] [] [] [] :
Equations
• =
theorem smul_eq_smul_iff_eq_and_eq_of_pos {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} [Zero α] [Zero β] [] [] [] [] [] (ha : a₁ a₂) (hb : b₁ b₂) (h₁ : 0 < a₁) (h₂ : 0 < b₂) :
a₁ b₁ = a₂ b₂ a₁ = a₂ b₁ = b₂
theorem smul_eq_smul_iff_eq_and_eq_of_pos' {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} [Zero α] [Zero β] [] [] [] [] [] (ha : a₁ a₂) (hb : b₁ b₂) (h₂ : 0 < a₂) (h₁ : 0 < b₁) :
a₁ b₁ = a₂ b₂ a₁ = a₂ b₁ = b₂
theorem pos_and_pos_or_neg_and_neg_of_smul_pos {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] [] (hab : 0 < a b) :
0 < a 0 < b a < 0 b < 0
theorem neg_of_smul_pos_right {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] [] (h : 0 < a b) (ha : a 0) :
b < 0
theorem neg_of_smul_pos_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] [] (h : 0 < a b) (ha : b 0) :
a < 0
theorem neg_iff_neg_of_smul_pos {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] [] (hab : 0 < a b) :
a < 0 b < 0
theorem neg_of_smul_neg_left' {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] (h : a b < 0) (ha : 0 a) :
b < 0
theorem neg_of_smul_neg_right' {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] (h : a b < 0) (hb : 0 b) :
a < 0
@[simp]
theorem le_smul_iff_one_le_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [] [Zero β] [] [] [] [] [] (hb : 0 < b) :
b a b 1 a
@[simp]
theorem lt_smul_iff_one_lt_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [] [Zero β] [] [] [] [] [] (hb : 0 < b) :
b < a b 1 < a
@[simp]
theorem smul_le_iff_le_one_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [] [Zero β] [] [] [] [] [] (hb : 0 < b) :
a b b a 1
@[simp]
theorem smul_lt_iff_lt_one_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [] [Zero β] [] [] [] [] [] (hb : 0 < b) :
a b < b a < 1
theorem smul_le_of_le_one_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [] [Zero β] [] [] [] [] (hb : 0 b) (h : a 1) :
a b b
theorem le_smul_of_one_le_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [] [Zero β] [] [] [] [] (hb : 0 b) (h : 1 a) :
b a b
theorem smul_lt_of_lt_one_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [] [Zero β] [] [] [] [] (hb : 0 < b) (h : a < 1) :
a b < b
theorem lt_smul_of_one_lt_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [] [Zero β] [] [] [] [] (hb : 0 < b) (h : 1 < a) :
b < a b
theorem PosSMulMono.toPosSMulStrictMono {α : Type u_1} {β : Type u_2} [] [] [Module α β] [] [] [] [] :
instance PosSMulReflectLT.toPosSMulReflectLE {α : Type u_1} {β : Type u_2} [] [] [Module α β] [] [] [] [] :
Equations
• =
theorem posSMulMono_iff_posSMulStrictMono {α : Type u_1} {β : Type u_2} [] [] [Module α β] [] [] [] :
theorem PosSMulReflectLE_iff_posSMulReflectLT {α : Type u_1} {β : Type u_2} [] [] [Module α β] [] [] [] :
theorem SMulPosMono.toSMulPosStrictMono {α : Type u_1} {β : Type u_2} [Ring α] [] [Module α β] [] [] [] [] :
theorem smulPosMono_iff_smulPosStrictMono {α : Type u_1} {β : Type u_2} [Ring α] [] [Module α β] [] [] [] :
theorem SMulPosReflectLT.toSMulPosReflectLE {α : Type u_1} {β : Type u_2} [Ring α] [] [Module α β] [] [] [] [] :
theorem SMulPosReflectLE_iff_smulPosReflectLT {α : Type u_1} {β : Type u_2} [Ring α] [] [Module α β] [] [] [] :
theorem inv_smul_le_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [] [] [] [] [] [] (ha : 0 < a) :
a⁻¹ b₁ b₂ b₁ a b₂
theorem le_inv_smul_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [] [] [] [] [] [] (ha : 0 < a) :
b₁ a⁻¹ b₂ a b₁ b₂
theorem inv_smul_lt_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [] [] [] [] [] [] (ha : 0 < a) :
a⁻¹ b₁ < b₂ b₁ < a b₂
theorem lt_inv_smul_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [] [] [] [] [] [] (ha : 0 < a) :
b₁ < a⁻¹ b₂ a b₁ < b₂
@[simp]
theorem OrderIso.smulRight_apply {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] {a : α} (ha : 0 < a) (b : β) :
() b = a b
@[simp]
theorem OrderIso.smulRight_symm_apply {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] {a : α} (ha : 0 < a) (b : β) :
() b = a⁻¹ b
def OrderIso.smulRight {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] {a : α} (ha : 0 < a) :
β ≃o β

Right scalar multiplication as an order isomorphism.

Equations
• = { toEquiv := , map_rel_iff' := }
Instances For
instance OrderDual.instPosSMulMono {α : Type u_1} {β : Type u_2} [] [] [SMul α β] [Zero α] [] :
Equations
• =
instance OrderDual.instPosSMulStrictMono {α : Type u_1} {β : Type u_2} [] [] [SMul α β] [Zero α] [] :
Equations
• =
instance OrderDual.instPosSMulReflectLT {α : Type u_1} {β : Type u_2} [] [] [SMul α β] [Zero α] [] :
Equations
• =
instance OrderDual.instPosSMulReflectLE {α : Type u_1} {β : Type u_2} [] [] [SMul α β] [Zero α] [] :
Equations
• =
instance OrderDual.instSMulPosMono {α : Type u_1} {β : Type u_2} [] [Ring α] [Module α β] [] :
Equations
• =
instance OrderDual.instSMulPosStrictMono {α : Type u_1} {β : Type u_2} [] [Ring α] [Module α β] [] :
Equations
• =
instance OrderDual.instSMulPosReflectLT {α : Type u_1} {β : Type u_2} [] [Ring α] [Module α β] [] :
Equations
• =
instance OrderDual.instSMulPosReflectLE {α : Type u_1} {β : Type u_2} [] [Ring α] [Module α β] [] :
Equations
• =
theorem smul_le_smul_of_nonpos_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [] [Module α β] [] (h : b₁ b₂) (ha : a 0) :
a b₂ a b₁
theorem antitone_smul_left {α : Type u_1} {β : Type u_2} {a : α} [] [Module α β] [] (ha : a 0) :
Antitone fun (x : β) => a x
instance PosSMulMono.toSMulPosMono {α : Type u_1} {β : Type u_2} [] [Module α β] [] :
Equations
• =
theorem smul_lt_smul_of_neg_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [] [Module α β] [] (hb : b₁ < b₂) (ha : a < 0) :
a b₂ < a b₁
theorem strictAnti_smul_left {α : Type u_1} {β : Type u_2} {a : α} [] [Module α β] [] (ha : a < 0) :
StrictAnti fun (x : β) => a x
instance PosSMulStrictMono.toSMulPosStrictMono {α : Type u_1} {β : Type u_2} [] [Module α β] [] :
Equations
• =
theorem le_of_smul_le_smul_of_neg {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [] [Module α β] [] (h : a b₁ a b₂) (ha : a < 0) :
b₂ b₁
theorem lt_of_smul_lt_smul_of_nonpos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [] [Module α β] [] (h : a b₁ < a b₂) (ha : a 0) :
b₂ < b₁
theorem smul_nonneg_of_nonpos_of_nonpos {α : Type u_1} {β : Type u_2} {a : α} {b : β} [] [Module α β] [] (ha : a 0) (hb : b 0) :
0 a b
theorem smul_le_smul_iff_of_neg_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [] [Module α β] [] [] (ha : a < 0) :
a b₁ a b₂ b₂ b₁
theorem smul_lt_smul_iff_of_neg_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [] [Module α β] [] [] (ha : a < 0) :
a b₁ < a b₂ b₂ < b₁
theorem smul_pos_iff_of_neg_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [] [Module α β] [] [] (ha : a < 0) :
0 < a b b < 0
theorem smul_pos_of_neg_of_neg {α : Type u_1} {β : Type u_2} {a : α} {b : β} [] [Module α β] [] [] (ha : a < 0) :
b < 00 < a b

Alias of the reverse direction of smul_pos_iff_of_neg_left.

theorem smul_neg_iff_of_neg_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [] [Module α β] [] [] (ha : a < 0) :
a b < 0 0 < b
theorem smul_add_smul_le_smul_add_smul {α : Type u_1} {β : Type u_2} [] [Module α β] [] [ContravariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x x_1] {b₁ : α} {b₂ : α} {a : β} {d : β} (hab : b₁ b₂) (hcd : a d) :
b₁ d + b₂ a b₁ a + b₂ d

Binary rearrangement inequality.

theorem smul_add_smul_le_smul_add_smul' {α : Type u_1} {β : Type u_2} [] [Module α β] [] [ContravariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x x_1] {b₁ : α} {b₂ : α} {a : β} {d : β} (hba : b₂ b₁) (hdc : d a) :
b₁ d + b₂ a b₁ a + b₂ d

Binary rearrangement inequality.

theorem smul_add_smul_lt_smul_add_smul {α : Type u_1} {β : Type u_2} [] [Module α β] [] [CovariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x < x_1] [ContravariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x < x_1] {b₁ : α} {b₂ : α} {a : β} {d : β} (hab : b₁ < b₂) (hcd : a < d) :
b₁ d + b₂ a < b₁ a + b₂ d

Binary strict rearrangement inequality.

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

Binary strict rearrangement inequality.

theorem smul_max_of_nonpos {α : Type u_1} {β : Type u_2} [] [Module α β] [] {a : α} (ha : a 0) (b₁ : β) (b₂ : β) :
a max b₁ b₂ = min (a b₁) (a b₂)
theorem smul_min_of_nonpos {α : Type u_1} {β : Type u_2} [] [Module α β] [] {a : α} (ha : a 0) (b₁ : β) (b₂ : β) :
a min b₁ b₂ = max (a b₁) (a b₂)
theorem nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg {α : Type u_1} {β : Type u_2} [Module α β] [] {a : α} {b : β} (hab : 0 a b) :
0 a 0 b a 0 b 0
theorem smul_nonneg_iff {α : Type u_1} {β : Type u_2} [Module α β] [] {a : α} {b : β} :
0 a b 0 a 0 b a 0 b 0
theorem smul_nonpos_iff {α : Type u_1} {β : Type u_2} [Module α β] [] {a : α} {b : β} :
a b 0 0 a b 0 a 0 0 b
theorem smul_nonneg_iff_pos_imp_nonneg {α : Type u_1} {β : Type u_2} [Module α β] [] {a : α} {b : β} :
0 a b (0 < a0 b) (0 < b0 a)
theorem smul_nonneg_iff_neg_imp_nonpos {α : Type u_1} {β : Type u_2} [Module α β] [] {a : α} {b : β} :
0 a b (a < 0b 0) (b < 0a 0)
theorem smul_nonpos_iff_pos_imp_nonpos {α : Type u_1} {β : Type u_2} [Module α β] [] {a : α} {b : β} :
a b 0 (0 < ab 0) (b < 00 a)
theorem smul_nonpos_iff_neg_imp_nonneg {α : Type u_1} {β : Type u_2} [Module α β] [] {a : α} {b : β} :
a b 0 (a < 00 b) (0 < ba 0)
@[instance 100]
instance PosSMulMono.toPosSMulReflectLE {α : Type u_1} {β : Type u_2} [] [] [] :
Equations
• =
@[instance 100]
instance PosSMulStrictMono.toPosSMulReflectLT {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
• =
theorem inv_smul_le_iff_of_neg {α : Type u_1} {β : Type u_2} [Module α β] {a : α} {b₁ : β} {b₂ : β} [] (h : a < 0) :
a⁻¹ b₁ b₂ a b₂ b₁
theorem smul_inv_le_iff_of_neg {α : Type u_1} {β : Type u_2} [Module α β] {a : α} {b₁ : β} {b₂ : β} [] (h : a < 0) :
b₁ a⁻¹ b₂ b₂ a b₁
@[simp]
theorem OrderIso.smulRightDual_symm_apply {α : Type u_1} (β : Type u_2) [Module α β] {a : α} [] (ha : a < 0) :
∀ (a_1 : βᵒᵈ), () a_1 = a⁻¹ OrderDual.ofDual a_1
@[simp]
theorem OrderIso.smulRightDual_apply {α : Type u_1} (β : Type u_2) [Module α β] {a : α} [] (ha : a < 0) :
∀ (a_1 : β), () a_1 = a OrderDual.toDual a_1
def OrderIso.smulRightDual {α : Type u_1} (β : Type u_2) [Module α β] {a : α} [] (ha : a < 0) :

Left scalar multiplication as an order isomorphism.

Equations
• = { toEquiv := ().trans OrderDual.toDual, map_rel_iff' := }
Instances For
theorem inv_smul_lt_iff_of_neg {α : Type u_1} {β : Type u_2} [Module α β] {a : α} {b₁ : β} {b₂ : β} [] (h : a < 0) :
a⁻¹ b₁ < b₂ a b₂ < b₁
theorem smul_inv_lt_iff_of_neg {α : Type u_1} {β : Type u_2} [Module α β] {a : α} {b₁ : β} {b₂ : β} [] (h : a < 0) :
b₁ < a⁻¹ b₂ b₂ < a b₁
instance Pi.instPosSMulMono {α : Type u_1} {ι : Type u_3} {β : ιType u_4} [Zero α] [(i : ι) → Zero (β i)] [] [(i : ι) → Preorder (β i)] [(i : ι) → SMulZeroClass α (β i)] [∀ (i : ι), PosSMulMono α (β i)] :
PosSMulMono α ((i : ι) → β i)
Equations
• =
instance Pi.instSMulPosMono {α : Type u_1} {ι : Type u_3} {β : ιType u_4} [(i : ι) → Zero (β i)] [] [(i : ι) → Preorder (β i)] [(i : ι) → SMulZeroClass α (β i)] [∀ (i : ι), SMulPosMono α (β i)] :
SMulPosMono α ((i : ι) → β i)
Equations
• =
instance Pi.instPosSMulReflectLE {α : Type u_1} {ι : Type u_3} {β : ιType u_4} [Zero α] [(i : ι) → Zero (β i)] [] [(i : ι) → Preorder (β i)] [(i : ι) → SMulZeroClass α (β i)] [∀ (i : ι), PosSMulReflectLE α (β i)] :
PosSMulReflectLE α ((i : ι) → β i)
Equations
• =
instance Pi.instSMulPosReflectLE {α : Type u_1} {ι : Type u_3} {β : ιType u_4} [(i : ι) → Zero (β i)] [] [(i : ι) → Preorder (β i)] [(i : ι) → SMulZeroClass α (β i)] [∀ (i : ι), SMulPosReflectLE α (β i)] :
SMulPosReflectLE α ((i : ι) → β i)
Equations
• =
instance Pi.instPosSMulStrictMono {α : Type u_1} {ι : Type u_3} {β : ιType u_4} [Zero α] [(i : ι) → Zero (β i)] [] [(i : ι) → PartialOrder (β i)] [(i : ι) → SMulWithZero α (β i)] [∀ (i : ι), PosSMulStrictMono α (β i)] :
PosSMulStrictMono α ((i : ι) → β i)
Equations
• =
instance Pi.instSMulPosStrictMono {α : Type u_1} {ι : Type u_3} {β : ιType u_4} [Zero α] [(i : ι) → Zero (β i)] [] [(i : ι) → PartialOrder (β i)] [(i : ι) → SMulWithZero α (β i)] [∀ (i : ι), SMulPosStrictMono α (β i)] :
SMulPosStrictMono α ((i : ι) → β i)
Equations
• =
instance Pi.instSMulPosReflectLT {α : Type u_1} {ι : Type u_3} {β : ιType u_4} [Zero α] [(i : ι) → Zero (β i)] [] [(i : ι) → PartialOrder (β i)] [(i : ι) → SMulWithZero α (β i)] [∀ (i : ι), SMulPosReflectLT α (β i)] :
SMulPosReflectLT α ((i : ι) → β i)
Equations
• =
theorem PosSMulMono.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero α] [] [] [] [SMul α β] [SMul α γ] (f : βγ) (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) [] :
theorem PosSMulStrictMono.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero α] [] [] [] [SMul α β] [SMul α γ] (f : βγ) (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) [] :
theorem PosSMulReflectLE.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero α] [] [] [] [SMul α β] [SMul α γ] (f : βγ) (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) [] :
theorem PosSMulReflectLT.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero α] [] [] [] [SMul α β] [SMul α γ] (f : βγ) (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) [] :
theorem SMulPosMono.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [Zero β] [] [Zero γ] [] [SMul α β] [SMul α γ] (f : βγ) (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) (zero : f 0 = 0) [] :
theorem SMulPosStrictMono.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [Zero β] [] [Zero γ] [] [SMul α β] [SMul α γ] (f : βγ) (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) (zero : f 0 = 0) [] :
theorem SMulPosReflectLE.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [Zero β] [] [Zero γ] [] [SMul α β] [SMul α γ] (f : βγ) (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) (zero : f 0 = 0) [] :
theorem SMulPosReflectLT.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [Zero β] [] [Zero γ] [] [SMul α β] [SMul α γ] (f : βγ) (hf : ∀ {b₁ b₂ : β}, f b₁ f b₂ b₁ b₂) (smul : ∀ (a : α) (b : β), f (a b) = a f b) (zero : f 0 = 0) [] :
instance OrderedSemiring.toPosSMulMonoNat {α : Type u_1} [] :
Equations
• =
instance OrderedSemiring.toSMulPosMonoNat {α : Type u_1} [] :
Equations
• =
Equations
• =
Equations
• =

Positivity extension for HSMul, i.e. (_ • _).

Equations
• One or more equations did not get rendered due to their size.
Instances For

### Deprecated lemmas #

Those lemmas have been deprecated on 2023-12-23.

@[deprecated monotone_smul_left_of_nonneg]
theorem monotone_smul_left {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [] [] [Zero α] [] (ha : 0 a) :
Monotone fun (x : β) => a x

Alias of monotone_smul_left_of_nonneg.

@[deprecated strictMono_smul_left_of_pos]
theorem strict_mono_smul_left {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [] [] [Zero α] [] (ha : 0 < a) :
StrictMono fun (x : β) => a x

Alias of strictMono_smul_left_of_pos.

@[deprecated smul_le_smul_of_nonneg_left]
theorem smul_le_smul_of_nonneg {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [] [] [Zero α] [] (hb : b₁ b₂) (ha : 0 a) :
a b₁ a b₂

Alias of smul_le_smul_of_nonneg_left.

@[deprecated smul_lt_smul_of_pos_left]
theorem smul_lt_smul_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [] [] [Zero α] [] (hb : b₁ < b₂) (ha : 0 < a) :
a b₁ < a b₂

Alias of smul_lt_smul_of_pos_left.

@[deprecated lt_of_smul_lt_smul_of_nonneg_left]
theorem lt_of_smul_lt_smul_of_nonneg {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [] [] [Zero α] [] (h : a b₁ < a b₂) (ha : 0 a) :
b₁ < b₂

Alias of lt_of_smul_lt_smul_left.

Alias of lt_of_smul_lt_smul_left.

@[deprecated smul_le_smul_iff_of_pos_left]
theorem smul_le_smul_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [] [] [Zero α] [] [] (ha : 0 < a) :
a b₁ a b₂ b₁ b₂

Alias of smul_le_smul_iff_of_pos_left.

@[deprecated smul_lt_smul_iff_of_pos_left]
theorem smul_lt_smul_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [SMul α β] [] [] [Zero α] [] [] (ha : 0 < a) :
a b₁ < a b₂ b₁ < b₂

Alias of smul_lt_smul_iff_of_pos_left.

@[deprecated smul_max_of_nonneg]
theorem smul_max {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [] [] [Zero α] [] (ha : 0 a) (b₁ : β) (b₂ : β) :
a max b₁ b₂ = max (a b₁) (a b₂)

Alias of smul_max_of_nonneg.

@[deprecated smul_min_of_nonneg]
theorem smul_min {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [] [] [Zero α] [] (ha : 0 a) (b₁ : β) (b₂ : β) :
a min b₁ b₂ = min (a b₁) (a b₂)

Alias of smul_min_of_nonneg.

@[deprecated smul_pos_iff_of_pos_left]
theorem smul_pos_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] [] (ha : 0 < a) :
0 < a b 0 < b

Alias of smul_pos_iff_of_pos_left.

@[deprecated inv_smul_le_iff_of_pos]
theorem inv_smul_le_iff {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [] [] [] [] [] [] (ha : 0 < a) :
a⁻¹ b₁ b₂ b₁ a b₂

Alias of inv_smul_le_iff_of_pos.

@[deprecated le_inv_smul_iff_of_pos]
theorem le_inv_smul_iff {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [] [] [] [] [] [] (ha : 0 < a) :
b₁ a⁻¹ b₂ a b₁ b₂

Alias of le_inv_smul_iff_of_pos.

@[deprecated inv_smul_lt_iff_of_pos]
theorem inv_smul_lt_iff {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [] [] [] [] [] [] (ha : 0 < a) :
a⁻¹ b₁ < b₂ b₁ < a b₂

Alias of inv_smul_lt_iff_of_pos.

@[deprecated lt_inv_smul_iff_of_pos]
theorem lt_inv_smul_iff {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [] [] [] [] [] [] (ha : 0 < a) :
b₁ < a⁻¹ b₂ a b₁ < b₂

Alias of lt_inv_smul_iff_of_pos.

@[deprecated OrderIso.smulRight]
def OrderIso.smulLeft {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] {a : α} (ha : 0 < a) :
β ≃o β

Alias of OrderIso.smulRight.

Right scalar multiplication as an order isomorphism.

Equations
Instances For
@[deprecated OrderIso.smulRight_symm_apply]
theorem OrderIso.smulLeft_symm_apply {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] {a : α} (ha : 0 < a) (b : β) :
() b = a⁻¹ b

Alias of OrderIso.smulRight_symm_apply.

@[deprecated OrderIso.smulRight_apply]
theorem OrderIso.smulLeft_apply {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] {a : α} (ha : 0 < a) (b : β) :
() b = a b

Alias of OrderIso.smulRight_apply.

@[deprecated smul_neg_iff_of_pos_left]
theorem smul_neg_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [] [] [] [] [] (ha : 0 < a) :
a b < 0 b < 0

Alias of smul_neg_iff_of_pos_left.

Those lemmas have been deprecated on 2023-12-27.

@[deprecated strictAnti_smul_left]
theorem strict_anti_smul_left {α : Type u_1} {β : Type u_2} {a : α} [] [Module α β] [] (ha : a < 0) :
StrictAnti fun (x : β) => a x

Alias of strictAnti_smul_left.

@[deprecated smul_le_smul_of_nonpos_left]
theorem smul_le_smul_of_nonpos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [] [Module α β] [] (h : b₁ b₂) (ha : a 0) :
a b₂ a b₁

Alias of smul_le_smul_of_nonpos_left.

@[deprecated smul_lt_smul_of_neg_left]
theorem smul_lt_smul_of_neg {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [] [Module α β] [] (hb : b₁ < b₂) (ha : a < 0) :
a b₂ < a b₁

Alias of smul_lt_smul_of_neg_left.

@[deprecated smul_pos_iff_of_neg_left]
theorem smul_pos_iff_of_neg {α : Type u_1} {β : Type u_2} {a : α} {b : β} [] [Module α β] [] [] (ha : a < 0) :
0 < a b b < 0

Alias of smul_pos_iff_of_neg_left.

@[deprecated smul_neg_iff_of_neg_left]
theorem smul_neg_iff_of_neg {α : Type u_1} {β : Type u_2} {a : α} {b : β} [] [Module α β] [] [] (ha : a < 0) :
a b < 0 0 < b

Alias of smul_neg_iff_of_neg_left.

@[deprecated smul_le_smul_iff_of_neg_left]
theorem smul_le_smul_iff_of_neg {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [] [Module α β] [] [] (ha : a < 0) :
a b₁ a b₂ b₂ b₁

Alias of smul_le_smul_iff_of_neg_left.

@[deprecated smul_lt_smul_iff_of_neg_left]
theorem smul_lt_smul_iff_of_neg {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [] [Module α β] [] [] (ha : a < 0) :
a b₁ < a b₂ b₂ < b₁

Alias of smul_lt_smul_iff_of_neg_left.