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:

• When α, β are partial orders:
  • PosSMulStrictMono → PosSMulMono
  • SMulPosStrictMono → SMulPosMono
  • PosSMulReflectLE → PosSMulReflectLT
  • SMulPosReflectLE → SMulPosReflectLT
• When β is a linear order:
  • PosSMulStrictMono → PosSMulReflectLE
  • PosSMulReflectLT → PosSMulMono (not registered as instance)
  • SMulPosReflectLT → SMulPosMono (not registered as instance)
  • PosSMulReflectLE → PosSMulStrictMono (not registered as instance)
  • SMulPosReflectLE → SMulPosStrictMono (not registered as instance)
• When α is a linear order:
  • SMulPosStrictMono → SMulPosReflectLE
• When α is an ordered ring, β an ordered group and also an α-module:
  • PosSMulMono → SMulPosMono
  • PosSMulStrictMono → SMulPosStrictMono
• When α is an linear ordered semifield, β is an α-module:
  • PosSMulStrictMono → PosSMulReflectLT
  • PosSMulMono → PosSMulReflectLE
• When α is a semiring, β is an α-module with NoZeroSMulDivisors:
  • PosSMulMono → PosSMulStrictMono (not registered as instance)
• When α is a ring, β is an α-module with NoZeroSMulDivisors:
  • SMulPosMono → SMulPosStrictMono (not registered as instance)

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

• OrderedSMul → PosSMulStrictMono
• OrderedSMul → PosSMulReflectLT

Unless otherwise stated, all these implications 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.GroupWithZero.Unbundled 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 α β] [Preorder α] [Preorder β] [Zero α] : Prop

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.

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

  Do not use this. Use smul_le_smul_of_nonneg_left instead.

theorem PosSMulMono.elim {α : Type u_1} {β : Type u_2} : ∀ {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero α} [self : PosSMulMono α β] ⦃a : α⦄, 0 ≤ a → ∀ ⦃b₁ b₂ : β⦄, 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 α β] [Preorder α] [Preorder β] [Zero α] : Prop

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.

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

  Do not use this. Use smul_lt_smul_of_pos_left instead.

theorem PosSMulStrictMono.elim {α : Type u_1} {β : Type u_2} : ∀ {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero α} [self : PosSMulStrictMono α β] ⦃a : α⦄, 0 < a → ∀ ⦃b₁ b₂ : β⦄, 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 α β] [Preorder α] [Preorder β] [Zero α] : Prop

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.

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

  Do not use this. Use lt_of_smul_lt_smul_left instead.

theorem PosSMulReflectLT.elim {α : Type u_1} {β : Type u_2} : ∀ {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero α} [self : PosSMulReflectLT α β] ⦃a : α⦄, 0 ≤ a → ∀ ⦃b₁ b₂ : β⦄, 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 α β] [Preorder α] [Preorder β] [Zero α] : Prop

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.

theorem PosSMulReflectLE.elim {α : Type u_1} {β : Type u_2} : ∀ {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero α} [self : PosSMulReflectLE α β] ⦃a : α⦄, 0 < a → ∀ ⦃b₁ b₂ : β⦄, 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 α β] [Preorder α] [Preorder β] [Zero β] : Prop

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.

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

  Do not use this. Use smul_le_smul_of_nonneg_right instead.

theorem SMulPosMono.elim {α : Type u_1} {β : Type u_2} : ∀ {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero β} [self : SMulPosMono α β] ⦃b : β⦄, 0 ≤ b → ∀ ⦃a₁ a₂ : α⦄, 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 α β] [Preorder α] [Preorder β] [Zero β] : Prop

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.

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

  Do not use this. Use smul_lt_smul_of_pos_right instead.

theorem SMulPosStrictMono.elim {α : Type u_1} {β : Type u_2} : ∀ {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero β} [self : SMulPosStrictMono α β] ⦃b : β⦄, 0 < b → ∀ ⦃a₁ a₂ : α⦄, 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 α β] [Preorder α] [Preorder β] [Zero β] : Prop

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.

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

  Do not use this. Use lt_of_smul_lt_smul_right instead.

theorem SMulPosReflectLT.elim {α : Type u_1} {β : Type u_2} : ∀ {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero β} [self : SMulPosReflectLT α β] ⦃b : β⦄, 0 ≤ b → ∀ ⦃a₁ a₂ : α⦄, 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 α β] [Preorder α] [Preorder β] [Zero β] : Prop

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₂ • b → a₁ ≤ a₂

  Do not use this. Use le_of_smul_lt_smul_right instead.

theorem SMulPosReflectLE.elim {α : Type u_1} {β : Type u_2} : ∀ {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero β} [self : SMulPosReflectLE α β] ⦃b : β⦄, 0 < b → ∀ ⦃a₁ a₂ : α⦄, 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 α] [Preorder α] [PosMulMono α] : PosSMulMono α α

Equations

• ⋯ = ⋯

@[instance 100]

instance PosMulStrictMono.toPosSMulStrictMono {α : Type u_1} [Zero α] [Mul α] [Preorder α] [PosMulStrictMono α] : PosSMulStrictMono α α

Equations

• ⋯ = ⋯

@[instance 100]

instance PosMulReflectLT.toPosSMulReflectLT {α : Type u_1} [Zero α] [Mul α] [Preorder α] [PosMulReflectLT α] : PosSMulReflectLT α α

Equations

• ⋯ = ⋯

@[instance 100]

instance PosMulReflectLE.toPosSMulReflectLE {α : Type u_1} [Zero α] [Mul α] [Preorder α] [PosMulReflectLE α] : PosSMulReflectLE α α

Equations

• ⋯ = ⋯

@[instance 100]

instance MulPosMono.toSMulPosMono {α : Type u_1} [Zero α] [Mul α] [Preorder α] [MulPosMono α] : SMulPosMono α α

Equations

• ⋯ = ⋯

@[instance 100]

instance MulPosStrictMono.toSMulPosStrictMono {α : Type u_1} [Zero α] [Mul α] [Preorder α] [MulPosStrictMono α] : SMulPosStrictMono α α

Equations

• ⋯ = ⋯

@[instance 100]

instance MulPosReflectLT.toSMulPosReflectLT {α : Type u_1} [Zero α] [Mul α] [Preorder α] [MulPosReflectLT α] : SMulPosReflectLT α α

Equations

• ⋯ = ⋯

@[instance 100]

instance MulPosReflectLE.toSMulPosReflectLE {α : Type u_1} [Zero α] [Mul α] [Preorder α] [MulPosReflectLE α] : SMulPosReflectLE α α

Equations

• ⋯ = ⋯

theorem monotone_smul_left_of_nonneg {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [Preorder α] [Preorder β] [Zero α] [PosSMulMono α β] (ha : 0 ≤ a) : Monotone fun (x : β) => a • x

theorem strictMono_smul_left_of_pos {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [Preorder α] [Preorder β] [Zero α] [PosSMulStrictMono α β] (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 α β] [Preorder α] [Preorder β] [Zero α] [PosSMulMono α β] (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 α β] [Preorder α] [Preorder β] [Zero α] [PosSMulStrictMono α β] (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 α β] [Preorder α] [Preorder β] [Zero α] [PosSMulReflectLT α β] (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 α β] [Preorder α] [Preorder β] [Zero α] [PosSMulReflectLE α β] (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 α β] [Preorder α] [Preorder β] [Zero α] [PosSMulReflectLT α β] (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 α β] [Preorder α] [Preorder β] [Zero α] [PosSMulReflectLE α β] (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 α β] [Preorder α] [Preorder β] [Zero α] [PosSMulMono α β] [PosSMulReflectLE α β] (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 α β] [Preorder α] [Preorder β] [Zero α] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) : a • b₁ < a • b₂ ↔ b₁ < b₂

theorem monotone_smul_right_of_nonneg {α : Type u_1} {β : Type u_2} {b : β} [SMul α β] [Preorder α] [Preorder β] [Zero β] [SMulPosMono α β] (hb : 0 ≤ b) : Monotone fun (x : α) => x • b

theorem strictMono_smul_right_of_pos {α : Type u_1} {β : Type u_2} {b : β} [SMul α β] [Preorder α] [Preorder β] [Zero β] [SMulPosStrictMono α β] (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 α β] [Preorder α] [Preorder β] [Zero β] [SMulPosMono α β] (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 α β] [Preorder α] [Preorder β] [Zero β] [SMulPosStrictMono α β] (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 α β] [Preorder α] [Preorder β] [Zero β] [SMulPosReflectLT α β] (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 α β] [Preorder α] [Preorder β] [Zero β] [SMulPosReflectLE α β] (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 α β] [Preorder α] [Preorder β] [Zero β] [SMulPosReflectLT α β] (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 α β] [Preorder α] [Preorder β] [Zero β] [SMulPosReflectLE α β] (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 α β] [Preorder α] [Preorder β] [Zero β] [SMulPosMono α β] [SMulPosReflectLE α β] (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 α β] [Preorder α] [Preorder β] [Zero β] [SMulPosStrictMono α β] [SMulPosReflectLT α β] (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 α β] [Preorder α] [Preorder β] [Zero α] [Zero β] [PosSMulStrictMono α β] [SMulPosMono α β] (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 α β] [Preorder α] [Preorder β] [Zero α] [Zero β] [PosSMulStrictMono α β] [SMulPosMono α β] (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 α β] [Preorder α] [Preorder β] [Zero α] [Zero β] [PosSMulMono α β] [SMulPosStrictMono α β] (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 α β] [Preorder α] [Preorder β] [Zero α] [Zero β] [PosSMulMono α β] [SMulPosStrictMono α β] (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 α β] [Preorder α] [Preorder β] [Zero α] [Zero β] [PosSMulStrictMono α β] [SMulPosStrictMono α β] (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 α β] [Preorder α] [Preorder β] [Zero α] [Zero β] [PosSMulStrictMono α β] [SMulPosStrictMono α β] (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 α β] [Preorder α] [Preorder β] [Zero α] [Zero β] [PosSMulMono α β] [SMulPosMono α β] (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 α β] [Preorder α] [Preorder β] [Zero α] [Zero β] [PosSMulMono α β] [SMulPosMono α β] (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 α β] [Preorder α] [LinearOrder β] [Zero α] [PosSMulStrictMono α β] : PosSMulReflectLE α β

Equations

• ⋯ = ⋯

theorem PosSMulReflectLE.toPosSMulStrictMono {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] [PosSMulReflectLE α β] : PosSMulStrictMono α β

theorem posSMulStrictMono_iff_PosSMulReflectLE {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] : PosSMulStrictMono α β ↔ PosSMulReflectLE α β

instance PosSMulMono.toPosSMulReflectLT {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] [PosSMulMono α β] : PosSMulReflectLT α β

Equations

• ⋯ = ⋯

theorem PosSMulReflectLT.toPosSMulMono {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] [PosSMulReflectLT α β] : PosSMulMono α β

theorem posSMulMono_iff_posSMulReflectLT {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] : PosSMulMono α β ↔ PosSMulReflectLT α β

theorem smul_max_of_nonneg {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] [PosSMulMono α β] (ha : 0 ≤ a) (b₁ : β) (b₂ : β) : a • (b₁ ⊔ b₂) = a • b₁ ⊔ a • b₂

theorem smul_min_of_nonneg {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] [PosSMulMono α β] (ha : 0 ≤ a) (b₁ : β) (b₂ : β) : a • (b₁ ⊓ b₂) = a • b₁ ⊓ a • b₂

theorem SMulPosReflectLE.toSMulPosStrictMono {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero β] [SMulPosReflectLE α β] : SMulPosStrictMono α β

theorem SMulPosReflectLT.toSMulPosMono {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero β] [SMulPosReflectLT α β] : SMulPosMono α β

@[instance 100]

instance SMulPosStrictMono.toSMulPosReflectLE {α : Type u_1} {β : Type u_2} [SMul α β] [LinearOrder α] [Preorder β] [Zero β] [SMulPosStrictMono α β] : SMulPosReflectLE α β

Equations

• ⋯ = ⋯

theorem SMulPosMono.toSMulPosReflectLT {α : Type u_1} {β : Type u_2} [SMul α β] [LinearOrder α] [Preorder β] [Zero β] [SMulPosMono α β] : SMulPosReflectLT α β

theorem smulPosStrictMono_iff_SMulPosReflectLE {α : Type u_1} {β : Type u_2} [SMul α β] [LinearOrder α] [LinearOrder β] [Zero β] : SMulPosStrictMono α β ↔ SMulPosReflectLE α β

theorem smulPosMono_iff_smulPosReflectLT {α : Type u_1} {β : Type u_2} [SMul α β] [LinearOrder α] [LinearOrder β] [Zero β] : SMulPosMono α β ↔ SMulPosReflectLT α β

theorem smul_pos {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulStrictMono α β] (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 β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulStrictMono α β] (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 β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (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 β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) : a • b < 0 ↔ b < 0

theorem smul_nonneg {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} [Zero α] [Zero β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulMono α β] (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 β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulMono α β] (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 β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulReflectLT α β] (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 β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulReflectLT α β] (h : a • b < 0) (ha : 0 ≤ a) : b < 0

theorem smul_pos' {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulWithZero α β] [Preorder α] [Preorder β] [SMulPosStrictMono α β] (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 β] [SMulWithZero α β] [Preorder α] [Preorder β] [SMulPosStrictMono α β] (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 β] [SMulWithZero α β] [Preorder α] [Preorder β] [SMulPosStrictMono α β] [SMulPosReflectLT α β] (hb : 0 < b) : 0 < a • b ↔ 0 < a

theorem smul_nonneg' {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} [Zero α] [Zero β] [SMulWithZero α β] [Preorder α] [Preorder β] [SMulPosMono α β] (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 β] [SMulWithZero α β] [Preorder α] [Preorder β] [SMulPosMono α β] (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 β] [SMulWithZero α β] [Preorder α] [Preorder β] [SMulPosReflectLT α β] (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 β] [SMulWithZero α β] [Preorder α] [Preorder β] [SMulPosReflectLT α β] (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 β] [SMulWithZero α β] [Preorder α] [Preorder β] [PosSMulReflectLT α β] [SMulPosReflectLT α β] (hab : 0 < a • b) : 0 < a ↔ 0 < b

theorem PosSMulMono.of_pos {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] [PartialOrder α] [Preorder β] (h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂) : PosSMulMono α β

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 β] [SMulWithZero α β] [PartialOrder α] [Preorder β] (h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂) : PosSMulReflectLT α β

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 β] [SMulWithZero α β] [Preorder α] [PartialOrder β] (h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b) : SMulPosMono α β

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 β] [SMulWithZero α β] [Preorder α] [PartialOrder β] (h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ • b < a₂ • b → a₁ < a₂) : SMulPosReflectLT α β

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 β] [SMulWithZero α β] [PartialOrder α] [PartialOrder β] [PosSMulStrictMono α β] : PosSMulMono α β

Equations

• ⋯ = ⋯

@[instance 100]

instance SMulPosStrictMono.toSMulPosMono {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] [PartialOrder α] [PartialOrder β] [SMulPosStrictMono α β] : SMulPosMono α β

Equations

• ⋯ = ⋯

@[instance 100]

instance PosSMulReflectLE.toPosSMulReflectLT {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] [PartialOrder α] [PartialOrder β] [PosSMulReflectLE α β] : PosSMulReflectLT α β

Equations

• ⋯ = ⋯

@[instance 100]

instance SMulPosReflectLE.toSMulPosReflectLT {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] [PartialOrder α] [PartialOrder β] [SMulPosReflectLE α β] : SMulPosReflectLT α β

Equations

• ⋯ = ⋯

theorem smul_eq_smul_iff_eq_and_eq_of_pos {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} [Zero α] [Zero β] [SMulWithZero α β] [PartialOrder α] [PartialOrder β] [PosSMulStrictMono α β] [SMulPosStrictMono α β] (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 β] [SMulWithZero α β] [PartialOrder α] [PartialOrder β] [PosSMulStrictMono α β] [SMulPosStrictMono α β] (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 β] [SMulWithZero α β] [LinearOrder α] [LinearOrder β] [PosSMulMono α β] [SMulPosMono α β] (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 β] [SMulWithZero α β] [LinearOrder α] [LinearOrder β] [PosSMulMono α β] [SMulPosMono α β] (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 β] [SMulWithZero α β] [LinearOrder α] [LinearOrder β] [PosSMulMono α β] [SMulPosMono α β] (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 β] [SMulWithZero α β] [LinearOrder α] [LinearOrder β] [PosSMulMono α β] [SMulPosMono α β] (hab : 0 < a • b) : a < 0 ↔ b < 0

theorem neg_of_smul_neg_left' {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Zero α] [Zero β] [SMulWithZero α β] [LinearOrder α] [LinearOrder β] [SMulPosMono α β] (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 β] [SMulWithZero α β] [LinearOrder α] [LinearOrder β] [PosSMulMono α β] (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 : β} [Monoid α] [Zero β] [MulAction α β] [Preorder α] [Preorder β] [SMulPosMono α β] [SMulPosReflectLE α β] (hb : 0 < b) : b ≤ a • b ↔ 1 ≤ a

@[simp]

theorem lt_smul_iff_one_lt_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Monoid α] [Zero β] [MulAction α β] [Preorder α] [Preorder β] [SMulPosStrictMono α β] [SMulPosReflectLT α β] (hb : 0 < b) : b < a • b ↔ 1 < a

@[simp]

theorem smul_le_iff_le_one_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Monoid α] [Zero β] [MulAction α β] [Preorder α] [Preorder β] [SMulPosMono α β] [SMulPosReflectLE α β] (hb : 0 < b) : a • b ≤ b ↔ a ≤ 1

@[simp]

theorem smul_lt_iff_lt_one_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Monoid α] [Zero β] [MulAction α β] [Preorder α] [Preorder β] [SMulPosStrictMono α β] [SMulPosReflectLT α β] (hb : 0 < b) : a • b < b ↔ a < 1

theorem smul_le_of_le_one_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Monoid α] [Zero β] [MulAction α β] [Preorder α] [Preorder β] [SMulPosMono α β] (hb : 0 ≤ b) (h : a ≤ 1) : a • b ≤ b

theorem le_smul_of_one_le_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Monoid α] [Zero β] [MulAction α β] [Preorder α] [Preorder β] [SMulPosMono α β] (hb : 0 ≤ b) (h : 1 ≤ a) : b ≤ a • b

theorem smul_lt_of_lt_one_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Monoid α] [Zero β] [MulAction α β] [Preorder α] [Preorder β] [SMulPosStrictMono α β] (hb : 0 < b) (h : a < 1) : a • b < b

theorem lt_smul_of_one_lt_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Monoid α] [Zero β] [MulAction α β] [Preorder α] [Preorder β] [SMulPosStrictMono α β] (hb : 0 < b) (h : 1 < a) : b < a • b

theorem PosSMulMono.toPosSMulStrictMono {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommGroup β] [Module α β] [NoZeroSMulDivisors α β] [Preorder α] [PartialOrder β] [PosSMulMono α β] : PosSMulStrictMono α β

instance PosSMulReflectLT.toPosSMulReflectLE {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommGroup β] [Module α β] [NoZeroSMulDivisors α β] [Preorder α] [PartialOrder β] [PosSMulReflectLT α β] : PosSMulReflectLE α β

Equations

• ⋯ = ⋯

theorem posSMulMono_iff_posSMulStrictMono {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommGroup β] [Module α β] [NoZeroSMulDivisors α β] [PartialOrder α] [PartialOrder β] : PosSMulMono α β ↔ PosSMulStrictMono α β

theorem PosSMulReflectLE_iff_posSMulReflectLT {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommGroup β] [Module α β] [NoZeroSMulDivisors α β] [PartialOrder α] [PartialOrder β] : PosSMulReflectLE α β ↔ PosSMulReflectLT α β

theorem SMulPosMono.toSMulPosStrictMono {α : Type u_1} {β : Type u_2} [Ring α] [AddCommGroup β] [Module α β] [NoZeroSMulDivisors α β] [PartialOrder α] [PartialOrder β] [SMulPosMono α β] : SMulPosStrictMono α β

theorem smulPosMono_iff_smulPosStrictMono {α : Type u_1} {β : Type u_2} [Ring α] [AddCommGroup β] [Module α β] [NoZeroSMulDivisors α β] [PartialOrder α] [PartialOrder β] : SMulPosMono α β ↔ SMulPosStrictMono α β

theorem SMulPosReflectLT.toSMulPosReflectLE {α : Type u_1} {β : Type u_2} [Ring α] [AddCommGroup β] [Module α β] [NoZeroSMulDivisors α β] [PartialOrder α] [PartialOrder β] [SMulPosReflectLT α β] : SMulPosReflectLE α β

theorem SMulPosReflectLE_iff_smulPosReflectLT {α : Type u_1} {β : Type u_2} [Ring α] [AddCommGroup β] [Module α β] [NoZeroSMulDivisors α β] [PartialOrder α] [PartialOrder β] : SMulPosReflectLE α β ↔ SMulPosReflectLT α β

theorem inv_smul_le_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β] (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₂ : β} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β] (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₂ : β} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (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₂ : β} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) : b₁ < a⁻¹ • b₂ ↔ a • b₁ < b₂

def OrderIso.smulRight {α : Type u_1} {β : Type u_2} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β] {a : α} (ha : 0 < a) : β ≃o β

Right scalar multiplication as an order isomorphism.

Equations

• OrderIso.smulRight ha = { toEquiv := Equiv.smulRight ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.smulRight_apply {α : Type u_1} {β : Type u_2} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β] {a : α} (ha : 0 < a) (b : β) : (OrderIso.smulRight ha) b = a • b

@[simp]

theorem OrderIso.smulRight_symm_apply {α : Type u_1} {β : Type u_2} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β] {a : α} (ha : 0 < a) (b : β) : (RelIso.symm (OrderIso.smulRight ha)) b = a⁻¹ • b

instance OrderDual.instPosSMulMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [SMul α β] [Zero α] [PosSMulMono α β] : PosSMulMono α βᵒᵈ

Equations

• ⋯ = ⋯

instance OrderDual.instPosSMulStrictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [SMul α β] [Zero α] [PosSMulStrictMono α β] : PosSMulStrictMono α βᵒᵈ

Equations

• ⋯ = ⋯

instance OrderDual.instPosSMulReflectLT {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [SMul α β] [Zero α] [PosSMulReflectLT α β] : PosSMulReflectLT α βᵒᵈ

Equations

• ⋯ = ⋯

instance OrderDual.instPosSMulReflectLE {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [SMul α β] [Zero α] [PosSMulReflectLE α β] : PosSMulReflectLE α βᵒᵈ

Equations

• ⋯ = ⋯

instance OrderDual.instSMulPosMono {α : Type u_1} {β : Type u_2} [Preorder α] [Monoid α] [OrderedAddCommGroup β] [DistribMulAction α β] [SMulPosMono α β] : SMulPosMono α βᵒᵈ

Equations

• ⋯ = ⋯

instance OrderDual.instSMulPosStrictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Monoid α] [OrderedAddCommGroup β] [DistribMulAction α β] [SMulPosStrictMono α β] : SMulPosStrictMono α βᵒᵈ

Equations

• ⋯ = ⋯

instance OrderDual.instSMulPosReflectLT {α : Type u_1} {β : Type u_2} [Preorder α] [Monoid α] [OrderedAddCommGroup β] [DistribMulAction α β] [SMulPosReflectLT α β] : SMulPosReflectLT α βᵒᵈ

Equations

• ⋯ = ⋯

instance OrderDual.instSMulPosReflectLE {α : Type u_1} {β : Type u_2} [Preorder α] [Monoid α] [OrderedAddCommGroup β] [DistribMulAction α β] [SMulPosReflectLE α β] : SMulPosReflectLE α βᵒᵈ

Equations

• ⋯ = ⋯

theorem smul_add_smul_le_smul_add_smul {α : Type u_1} {β : Type u_2} [StrictOrderedSemiring α] [ExistsAddOfLE α] [OrderedCancelAddCommMonoid β] [Module α β] [PosSMulMono α β] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) : a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂

Binary rearrangement inequality.

theorem smul_add_smul_le_smul_add_smul' {α : Type u_1} {β : Type u_2} [StrictOrderedSemiring α] [ExistsAddOfLE α] [OrderedCancelAddCommMonoid β] [Module α β] [PosSMulMono α β] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} (ha : a₂ ≤ a₁) (hb : b₂ ≤ b₁) : a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂

Binary rearrangement inequality.

theorem smul_add_smul_lt_smul_add_smul {α : Type u_1} {β : Type u_2} [StrictOrderedSemiring α] [ExistsAddOfLE α] [OrderedCancelAddCommMonoid β] [Module α β] [PosSMulStrictMono α β] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} (ha : a₁ < a₂) (hb : b₁ < b₂) : a₁ • b₂ + a₂ • b₁ < a₁ • b₁ + a₂ • b₂

Binary strict rearrangement inequality.

theorem smul_add_smul_lt_smul_add_smul' {α : Type u_1} {β : Type u_2} [StrictOrderedSemiring α] [ExistsAddOfLE α] [OrderedCancelAddCommMonoid β] [Module α β] [PosSMulStrictMono α β] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} (ha : a₂ < a₁) (hb : b₂ < b₁) : a₁ • b₂ + a₂ • b₁ < a₁ • b₁ + a₂ • b₂

Binary strict rearrangement inequality.

theorem smul_le_smul_of_nonpos_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulMono α β] (h : b₁ ≤ b₂) (ha : a ≤ 0) : a • b₂ ≤ a • b₁

theorem antitone_smul_left {α : Type u_1} {β : Type u_2} {a : α} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulMono α β] (ha : a ≤ 0) : Antitone fun (x : β) => a • x

instance PosSMulMono.toSMulPosMono {α : Type u_1} {β : Type u_2} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulMono α β] : SMulPosMono α β

Equations

• ⋯ = ⋯

theorem smul_lt_smul_of_neg_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] (hb : b₁ < b₂) (ha : a < 0) : a • b₂ < a • b₁

theorem strictAnti_smul_left {α : Type u_1} {β : Type u_2} {a : α} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] (ha : a < 0) : StrictAnti fun (x : β) => a • x

instance PosSMulStrictMono.toSMulPosStrictMono {α : Type u_1} {β : Type u_2} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] : SMulPosStrictMono α β

Equations

• ⋯ = ⋯

theorem le_of_smul_le_smul_of_neg {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulReflectLE α β] (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₂ : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulReflectLT α β] (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 : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [SMulPosMono α β] (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₂ : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulMono α β] [PosSMulReflectLE α β] (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₂ : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : a < 0) : a • b₁ < a • b₂ ↔ b₂ < b₁

theorem smul_pos_iff_of_neg_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : a < 0) : 0 < a • b ↔ b < 0

theorem smul_pos_of_neg_of_neg {α : Type u_1} {β : Type u_2} {a : α} {b : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : a < 0) : b < 0 → 0 < 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 : β} [OrderedRing α] [OrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : a < 0) : a • b < 0 ↔ 0 < b

theorem smul_max_of_nonpos {α : Type u_1} {β : Type u_2} [OrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [PosSMulMono α β] {a : α} (ha : a ≤ 0) (b₁ : β) (b₂ : β) : a • (b₁ ⊔ b₂) = a • b₁ ⊓ a • b₂

theorem smul_min_of_nonpos {α : Type u_1} {β : Type u_2} [OrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [PosSMulMono α β] {a : α} (ha : a ≤ 0) (b₁ : β) (b₂ : β) : a • (b₁ ⊓ b₂) = a • b₁ ⊔ a • b₂

theorem nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg {α : Type u_1} {β : Type u_2} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} (hab : 0 ≤ a • b) : 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

theorem smul_nonneg_iff {α : Type u_1} {β : Type u_2} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} : 0 ≤ a • b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

theorem smul_nonpos_iff {α : Type u_1} {β : Type u_2} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] {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} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} : 0 ≤ a • b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)

theorem smul_nonneg_iff_neg_imp_nonpos {α : Type u_1} {β : Type u_2} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} : 0 ≤ a • b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

theorem smul_nonpos_iff_pos_imp_nonpos {α : Type u_1} {β : Type u_2} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} : a • b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

theorem smul_nonpos_iff_neg_imp_nonneg {α : Type u_1} {β : Type u_2} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} : a • b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

@[instance 100]

instance PosSMulMono.toPosSMulReflectLE {α : Type u_1} {β : Type u_2} [LinearOrderedSemifield α] [PartialOrder β] [MulAction α β] [PosSMulMono α β] : PosSMulReflectLE α β

Equations

• ⋯ = ⋯

@[instance 100]

instance PosSMulStrictMono.toPosSMulReflectLT {α : Type u_1} {β : Type u_2} [LinearOrderedSemifield α] [AddCommGroup β] [PartialOrder β] [MulActionWithZero α β] [PosSMulStrictMono α β] : PosSMulReflectLT α β

Equations

• ⋯ = ⋯

theorem inv_smul_le_iff_of_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [OrderedAddCommGroup β] [Module α β] {a : α} {b₁ : β} {b₂ : β} [PosSMulMono α β] (h : a < 0) : a⁻¹ • b₁ ≤ b₂ ↔ a • b₂ ≤ b₁

theorem smul_inv_le_iff_of_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [OrderedAddCommGroup β] [Module α β] {a : α} {b₁ : β} {b₂ : β} [PosSMulMono α β] (h : a < 0) : b₁ ≤ a⁻¹ • b₂ ↔ b₂ ≤ a • b₁

def OrderIso.smulRightDual {α : Type u_1} (β : Type u_2) [LinearOrderedField α] [OrderedAddCommGroup β] [Module α β] {a : α} [PosSMulMono α β] (ha : a < 0) : β ≃o βᵒᵈ

Left scalar multiplication as an order isomorphism.

Equations

• OrderIso.smulRightDual β ha = { toEquiv := (Equiv.smulRight ⋯).trans OrderDual.toDual, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.smulRightDual_apply {α : Type u_1} (β : Type u_2) [LinearOrderedField α] [OrderedAddCommGroup β] [Module α β] {a : α} [PosSMulMono α β] (ha : a < 0) : ∀ (a_1 : β), (OrderIso.smulRightDual β ha) a_1 = a • OrderDual.toDual a_1

@[simp]

theorem OrderIso.smulRightDual_symm_apply {α : Type u_1} (β : Type u_2) [LinearOrderedField α] [OrderedAddCommGroup β] [Module α β] {a : α} [PosSMulMono α β] (ha : a < 0) : ∀ (a_1 : βᵒᵈ), (RelIso.symm (OrderIso.smulRightDual β ha)) a_1 = a⁻¹ • OrderDual.ofDual a_1

theorem inv_smul_lt_iff_of_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [OrderedAddCommGroup β] [Module α β] {a : α} {b₁ : β} {b₂ : β} [PosSMulStrictMono α β] (h : a < 0) : a⁻¹ • b₁ < b₂ ↔ a • b₂ < b₁

theorem smul_inv_lt_iff_of_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [OrderedAddCommGroup β] [Module α β] {a : α} {b₁ : β} {b₂ : β} [PosSMulStrictMono α β] (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)] [Preorder α] [(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)] [Preorder α] [(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)] [Preorder α] [(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)] [Preorder α] [(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)] [PartialOrder α] [(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)] [PartialOrder α] [(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)] [PartialOrder α] [(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} [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] (f : β → γ) [Zero α] [PosSMulMono α γ] (hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂) (smul : ∀ (a : α) (b : β), f (a • b) = a • f b) : PosSMulMono α β

theorem PosSMulStrictMono.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] (f : β → γ) [Zero α] [PosSMulStrictMono α γ] (hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂) (smul : ∀ (a : α) (b : β), f (a • b) = a • f b) : PosSMulStrictMono α β

theorem PosSMulReflectLE.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] (f : β → γ) [Zero α] [PosSMulReflectLE α γ] (hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂) (smul : ∀ (a : α) (b : β), f (a • b) = a • f b) : PosSMulReflectLE α β

theorem PosSMulReflectLT.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] (f : β → γ) [Zero α] [PosSMulReflectLT α γ] (hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂) (smul : ∀ (a : α) (b : β), f (a • b) = a • f b) : PosSMulReflectLT α β

theorem SMulPosMono.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] (f : β → γ) [Zero β] [Zero γ] [SMulPosMono α γ] (hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂) (smul : ∀ (a : α) (b : β), f (a • b) = a • f b) (zero : f 0 = 0) : SMulPosMono α β

theorem SMulPosStrictMono.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] (f : β → γ) [Zero β] [Zero γ] [SMulPosStrictMono α γ] (hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂) (smul : ∀ (a : α) (b : β), f (a • b) = a • f b) (zero : f 0 = 0) : SMulPosStrictMono α β

theorem SMulPosReflectLE.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] (f : β → γ) [Zero β] [Zero γ] [SMulPosReflectLE α γ] (hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂) (smul : ∀ (a : α) (b : β), f (a • b) = a • f b) (zero : f 0 = 0) : SMulPosReflectLE α β

theorem SMulPosReflectLT.lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] (f : β → γ) [Zero β] [Zero γ] [SMulPosReflectLT α γ] (hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂) (smul : ∀ (a : α) (b : β), f (a • b) = a • f b) (zero : f 0 = 0) : SMulPosReflectLT α β

instance OrderedSemiring.toPosSMulMonoNat {α : Type u_1} [OrderedSemiring α] : PosSMulMono ℕ α

Equations

• ⋯ = ⋯

instance OrderedSemiring.toSMulPosMonoNat {α : Type u_1} [OrderedSemiring α] : SMulPosMono ℕ α

Equations

• ⋯ = ⋯

instance StrictOrderedSemiring.toPosSMulStrictMonoNat {α : Type u_1} [StrictOrderedSemiring α] : PosSMulStrictMono ℕ α

Equations

• ⋯ = ⋯

instance StrictOrderedSemiring.toSMulPosStrictMonoNat {α : Type u_1} [StrictOrderedSemiring α] : SMulPosStrictMono ℕ α

Equations

• ⋯ = ⋯

def Mathlib.Meta.Positivity.evalHSMul : Mathlib.Meta.Positivity.PositivityExt

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

Equations

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