# 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 `IsOrderedAddMonoid` and `IsOrderedModule` 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₂`.

Furthermore, in a module, i.e. a group acted on by a ring, `PosSMulMono` and `SMulPosMono` are equivalent (they are both the same as `∀ r ≥ 0, ∀ m ≥ 0, 0 ≤ r • m`), and similarly for `PosSMulStrictMono` and `SMulPosStrictMono`. To avoid dangerous instances going both, we have the extra two typeclasses:

- `IsOrderedModule`: Conjunction of `PosSMulMono` and `SMulPosMono`
- `IsStrictOrderedModule`: Conjunction of `PosSMulStrictMono` and `SMulPosStrictMono`.

## 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:

- `IsOrderedModule → PosSMulMono`
- `IsOrderedModule → SMulPosMono`
- `IsStrictOrderedModule → PosSMulStrictMono`
- `IsStrictOrderedModule → SMulPosStrictMono`

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.lean` custom typeclasses too.

source
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 `IsOrderedModule`.

- smul_le_smul_of_nonneg_left ⦃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.

Instances

source
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 `IsOrderedModule`.

- smul_lt_smul_of_pos_left ⦃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.

Instances

source
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 `IsOrderedModule`.

- lt_of_smul_lt_smul_left ⦃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.

Instances

source
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 `IsOrderedModule`.

- le_of_smul_le_smul_left ⦃a : α⦄ (ha : 0 < a) ⦃b₁ b₂ : β⦄ (hb : a • b₁ ≤ a • b₂) : b₁ ≤ b₂

  Do not use this. Use `le_of_smul_le_smul_left` instead.

Instances

source
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 `IsOrderedModule`.

- smul_le_smul_of_nonneg_right ⦃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.

Instances

source
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 `IsOrderedModule`.

- smul_lt_smul_of_pos_right ⦃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.

Instances

source
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 `IsOrderedModule`.

- lt_of_smul_lt_smul_right ⦃b : β⦄ (hb : 0 ≤ b) ⦃a₁ a₂ : α⦄ : a₁ • b < a₂ • b → a₁ < a₂

  Do not use this. Use `lt_of_smul_lt_smul_right` instead.

Instances

source
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 `IsOrderedModule`.

- le_of_smul_le_smul_right ⦃b : β⦄ (hb : 0 < b) ⦃a₁ a₂ : α⦄ : a₁ • b ≤ a₂ • b → a₁ ≤ a₂

  Do not use this. Use `le_of_smul_le_smul_right` instead.

Instances

source
class IsOrderedModule (α : Type u_1) (β : Type u_2) [SMul α β] [Preorder α] [Preorder β] [Zero α] [Zero β] extends PosSMulMono α β, SMulPosMono α β :
Prop

An ordered module is a module with a partial order such that scalar multiplication by a nonnegative scalar and of a nonnegative vector are both monotone.

- smul_le_smul_of_nonneg_left ⦃a : α⦄ (ha : 0 ≤ a) ⦃b₁ b₂ : β⦄ (hb : b₁ ≤ b₂) : a • b₁ ≤ a • b₂
- smul_le_smul_of_nonneg_right ⦃b : β⦄ (hb : 0 ≤ b) ⦃a₁ a₂ : α⦄ (ha : a₁ ≤ a₂) : a₁ • b ≤ a₂ • b

Instances

source
class IsStrictOrderedModule (α : Type u_1) (β : Type u_2) [SMul α β] [Preorder α] [Preorder β] [Zero α] [Zero β] extends PosSMulStrictMono α β, SMulPosStrictMono α β :
Prop

An ordered module is a module with a partial order such that scalar multiplication by a positive scalar and of a positive vector are both strictly monotone.

- smul_lt_smul_of_pos_left ⦃a : α⦄ (ha : 0 < a) ⦃b₁ b₂ : β⦄ (hb : b₁ < b₂) : a • b₁ < a • b₂
- smul_lt_smul_of_pos_right ⦃b : β⦄ (hb : 0 < b) ⦃a₁ a₂ : α⦄ (ha : a₁ < a₂) : a₁ • b < a₂ • b

Instances

source
@[instance 100]
instance PosMulMono.toPosSMulMono {α : Type u_1} [Zero α] [Mul α] [Preorder α] [PosMulMono α] :
PosSMulMono α α
source
@[instance 100]
instance PosMulStrictMono.toPosSMulStrictMono {α : Type u_1} [Zero α] [Mul α] [Preorder α] [PosMulStrictMono α] :
PosSMulStrictMono α α
source
@[instance 100]
instance PosMulReflectLT.toPosSMulReflectLT {α : Type u_1} [Zero α] [Mul α] [Preorder α] [PosMulReflectLT α] :
PosSMulReflectLT α α
source
@[instance 100]
instance PosMulReflectLE.toPosSMulReflectLE {α : Type u_1} [Zero α] [Mul α] [Preorder α] [PosMulReflectLE α] :
PosSMulReflectLE α α
source
@[instance 100]
instance MulPosMono.toSMulPosMono {α : Type u_1} [Zero α] [Mul α] [Preorder α] [MulPosMono α] :
SMulPosMono α α
source
@[instance 100]
instance MulPosStrictMono.toSMulPosStrictMono {α : Type u_1} [Zero α] [Mul α] [Preorder α] [MulPosStrictMono α] :
SMulPosStrictMono α α
source
@[instance 100]
instance MulPosReflectLT.toSMulPosReflectLT {α : Type u_1} [Zero α] [Mul α] [Preorder α] [MulPosReflectLT α] :
SMulPosReflectLT α α
source
@[instance 100]
instance MulPosReflectLE.toSMulPosReflectLE {α : Type u_1} [Zero α] [Mul α] [Preorder α] [MulPosReflectLE α] :
SMulPosReflectLE α α
source
instance instPosSMulMonoNatOfIsOrderedAddMonoid {M : Type u_3} [PartialOrder M] [AddCommMonoid M] [IsOrderedAddMonoid M] :
PosSMulMono ℕ M
source
instance instSMulPosMonoNatOfIsOrderedAddMonoid {M : Type u_3} [PartialOrder M] [AddCommMonoid M] [IsOrderedAddMonoid M] :
SMulPosMono ℕ M
source
instance instPosSMulStrictMonoNatOfIsOrderedAddMonoid {M : Type u_3} [PartialOrder M] [AddCancelCommMonoid M] [IsOrderedAddMonoid M] :
PosSMulStrictMono ℕ M
source
instance instSMulPosStrictMonoNatOfIsOrderedCancelAddMonoid {M : Type u_3} [PartialOrder M] [AddCommMonoid M] [IsOrderedCancelAddMonoid M] :
SMulPosStrictMono ℕ M
source
instance instPosSMulStrictMonoIntOfIsOrderedAddMonoid {G : Type u_3} [PartialOrder G] [AddCommGroup G] [IsOrderedAddMonoid G] :
PosSMulStrictMono ℤ G
source
instance instSMulPosStrictMonoIntOfIsOrderedAddMonoid {G : Type u_3} [PartialOrder G] [AddCommGroup G] [IsOrderedAddMonoid G] :
SMulPosStrictMono ℤ G
source
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
source
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
source
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₂
source
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₂
source
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₂
source
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₂
source
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`.

source
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`.

source
@[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₂
source
@[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₂
source
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
source
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
source
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
source
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
source
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₂
source
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₂
source
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`.

source
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`.

source
@[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₂
source
@[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₂
source
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₂
source
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₂
source
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₂
source
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₂
source
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₂
source
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₂
source
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₂
source
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₂
source
@[instance 100]
instance IsOrderedRing.toIsOrderedModule {α : Type u_1} [Semiring α] [PartialOrder α] [IsOrderedRing α] :
IsOrderedModule α α
source
@[instance 100]
instance IsStrictOrderedRing.toIsStrictOrderedModule {α : Type u_1} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] :
IsStrictOrderedModule α α
source
@[instance 100]
instance PosSMulStrictMono.toPosSMulReflectLE {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] [PosSMulStrictMono α β] :
PosSMulReflectLE α β
source
theorem PosSMulReflectLE.toPosSMulStrictMono {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] [PosSMulReflectLE α β] :
PosSMulStrictMono α β
source
theorem posSMulStrictMono_iff_PosSMulReflectLE {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] :
PosSMulStrictMono α β ↔ PosSMulReflectLE α β
source
instance PosSMulMono.toPosSMulReflectLT {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] [PosSMulMono α β] :
PosSMulReflectLT α β
source
theorem PosSMulReflectLT.toPosSMulMono {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] [PosSMulReflectLT α β] :
PosSMulMono α β
source
theorem posSMulMono_iff_posSMulReflectLT {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] :
PosSMulMono α β ↔ PosSMulReflectLT α β
source
theorem smul_max_of_nonneg {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] [PosSMulMono α β] (ha : 0 ≤ a) (b₁ b₂ : β) :
a • max b₁ b₂ = max (a • b₁) (a • b₂)
source
theorem smul_min_of_nonneg {α : Type u_1} {β : Type u_2} {a : α} [SMul α β] [Preorder α] [LinearOrder β] [Zero α] [PosSMulMono α β] (ha : 0 ≤ a) (b₁ b₂ : β) :
a • min b₁ b₂ = min (a • b₁) (a • b₂)
source
theorem SMulPosReflectLE.toSMulPosStrictMono {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero β] [SMulPosReflectLE α β] :
SMulPosStrictMono α β
source
theorem SMulPosReflectLT.toSMulPosMono {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [LinearOrder β] [Zero β] [SMulPosReflectLT α β] :
SMulPosMono α β
source
@[instance 100]
instance SMulPosStrictMono.toSMulPosReflectLE {α : Type u_1} {β : Type u_2} [SMul α β] [LinearOrder α] [Preorder β] [Zero β] [SMulPosStrictMono α β] :
SMulPosReflectLE α β
source
theorem SMulPosMono.toSMulPosReflectLT {α : Type u_1} {β : Type u_2} [SMul α β] [LinearOrder α] [Preorder β] [Zero β] [SMulPosMono α β] :
SMulPosReflectLT α β
source
theorem smulPosStrictMono_iff_SMulPosReflectLE {α : Type u_1} {β : Type u_2} [SMul α β] [LinearOrder α] [LinearOrder β] [Zero β] :
SMulPosStrictMono α β ↔ SMulPosReflectLE α β
source
theorem smulPosMono_iff_smulPosReflectLT {α : Type u_1} {β : Type u_2} [SMul α β] [LinearOrder α] [LinearOrder β] [Zero β] :
SMulPosMono α β ↔ SMulPosReflectLT α β
source
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
source
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
source
@[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
source
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
source
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₁
source
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
source
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
source
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
source
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
source
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
source
@[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
source
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₁
source
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
source
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
source
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
source
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
source
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`

source
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`

source
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`

source
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`

source
@[instance 100]
instance PosSMulStrictMono.toPosSMulMono {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] [PartialOrder α] [PartialOrder β] [PosSMulStrictMono α β] :
PosSMulMono α β
source
@[instance 100]
instance SMulPosStrictMono.toSMulPosMono {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] [PartialOrder α] [PartialOrder β] [SMulPosStrictMono α β] :
SMulPosMono α β
source
@[instance 100]
instance PosSMulReflectLE.toPosSMulReflectLT {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] [PartialOrder α] [PartialOrder β] [PosSMulReflectLE α β] :
PosSMulReflectLT α β
source
@[instance 100]
instance SMulPosReflectLE.toSMulPosReflectLT {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] [PartialOrder α] [PartialOrder β] [SMulPosReflectLE α β] :
SMulPosReflectLT α β
source
@[instance 100]
instance IsStrictOrderedModule.toIsOrderedModule {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] [PartialOrder α] [PartialOrder β] [IsStrictOrderedModule α β] :
IsOrderedModule α β
source
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₂
source
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₂
source
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
source
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
source
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
source
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
source
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
source
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
source
@[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
source
@[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
source
@[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
source
@[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
source
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
source
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
source
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
source
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
source
theorem PosSMulMono.of_smul_nonneg {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommGroup β] [Module α β] [PartialOrder α] [PartialOrder β] [IsOrderedAddMonoid β] (h : ∀ (a : α), 0 ≤ a → ∀ (b : β), 0 ≤ b → 0 ≤ a • b) :
PosSMulMono α β

Constructor for `PosSMulMono` when the semimodule is in fact a group.

source
theorem PosSMulMono.toPosSMulStrictMono {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommGroup β] [Module α β] [NoZeroSMulDivisors α β] [Preorder α] [PartialOrder β] [PosSMulMono α β] :
PosSMulStrictMono α β
source
instance PosSMulReflectLT.toPosSMulReflectLE {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommGroup β] [Module α β] [NoZeroSMulDivisors α β] [Preorder α] [PartialOrder β] [PosSMulReflectLT α β] :
PosSMulReflectLE α β
source
theorem posSMulMono_iff_posSMulStrictMono {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommGroup β] [Module α β] [NoZeroSMulDivisors α β] [PartialOrder α] [PartialOrder β] :
PosSMulMono α β ↔ PosSMulStrictMono α β
source
theorem PosSMulReflectLE_iff_posSMulReflectLT {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommGroup β] [Module α β] [NoZeroSMulDivisors α β] [PartialOrder α] [PartialOrder β] :
PosSMulReflectLE α β ↔ PosSMulReflectLT α β
source
theorem IsOrderedModule.of_smul_nonneg {α : Type u_1} {β : Type u_2} [Ring α] [AddCommGroup β] [Module α β] [PartialOrder α] [PartialOrder β] [IsOrderedAddMonoid α] [IsOrderedAddMonoid β] (h : ∀ (a : α), 0 ≤ a → ∀ (b : β), 0 ≤ b → 0 ≤ a • b) :
IsOrderedModule α β

Constructor for `IsOrderedModule` when the semimodule is in fact a module.

source
theorem SMulPosMono.toSMulPosStrictMono {α : Type u_1} {β : Type u_2} [Ring α] [AddCommGroup β] [Module α β] [PartialOrder α] [PartialOrder β] [NoZeroSMulDivisors α β] [SMulPosMono α β] :
SMulPosStrictMono α β
source
theorem smulPosMono_iff_smulPosStrictMono {α : Type u_1} {β : Type u_2} [Ring α] [AddCommGroup β] [Module α β] [PartialOrder α] [PartialOrder β] [NoZeroSMulDivisors α β] :
SMulPosMono α β ↔ SMulPosStrictMono α β
source
theorem SMulPosReflectLT.toSMulPosReflectLE {α : Type u_1} {β : Type u_2} [Ring α] [AddCommGroup β] [Module α β] [PartialOrder α] [PartialOrder β] [NoZeroSMulDivisors α β] [SMulPosReflectLT α β] :
SMulPosReflectLE α β
source
theorem SMulPosReflectLE_iff_smulPosReflectLT {α : Type u_1} {β : Type u_2} [Ring α] [AddCommGroup β] [Module α β] [PartialOrder α] [PartialOrder β] [NoZeroSMulDivisors α β] :
SMulPosReflectLE α β ↔ SMulPosReflectLT α β
source
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₂
source
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₂
source
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₂
source
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₂
source
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' := ⋯ }

Instances For

source
@[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 (smulRight ha)) b = a⁻¹ • b
source
@[simp]
theorem OrderIso.smulRight_apply {α : Type u_1} {β : Type u_2} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β] {a : α} (ha : 0 < a) (b : β) :
(smulRight ha) b = a • b
source
instance OrderDual.instPosSMulMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [SMul α β] [Zero α] [PosSMulMono α β] :
PosSMulMono α β ᵒᵈ
source
instance OrderDual.instPosSMulStrictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [SMul α β] [Zero α] [PosSMulStrictMono α β] :
PosSMulStrictMono α β ᵒᵈ
source
instance OrderDual.instPosSMulReflectLT {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [SMul α β] [Zero α] [PosSMulReflectLT α β] :
PosSMulReflectLT α β ᵒᵈ
source
instance OrderDual.instPosSMulReflectLE {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [SMul α β] [Zero α] [PosSMulReflectLE α β] :
PosSMulReflectLE α β ᵒᵈ
source
instance OrderDual.instSMulPosMono {α : Type u_1} {β : Type u_2} [Preorder α] [Monoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [DistribMulAction α β] [SMulPosMono α β] :
SMulPosMono α β ᵒᵈ
source
instance OrderDual.instSMulPosStrictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Monoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [DistribMulAction α β] [SMulPosStrictMono α β] :
SMulPosStrictMono α β ᵒᵈ
source
instance OrderDual.instSMulPosReflectLT {α : Type u_1} {β : Type u_2} [Preorder α] [Monoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [DistribMulAction α β] [SMulPosReflectLT α β] :
SMulPosReflectLT α β ᵒᵈ
source
instance OrderDual.instSMulPosReflectLE {α : Type u_1} {β : Type u_2} [Preorder α] [Monoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [DistribMulAction α β] [SMulPosReflectLE α β] :
SMulPosReflectLE α β ᵒᵈ
source
instance OrderDual.instIsOrderedModule {α : Type u_1} {β : Type u_2} [Preorder α] [MonoidWithZero α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [DistribMulAction α β] [IsOrderedModule α β] :
IsOrderedModule α β ᵒᵈ
source
instance OrderDual.instIsStrictOrderedModule {α : Type u_1} {β : Type u_2} [Preorder α] [MonoidWithZero α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [DistribMulAction α β] [IsStrictOrderedModule α β] :
IsStrictOrderedModule α β ᵒᵈ
source
theorem smul_add_smul_le_smul_add_smul {α : Type u_1} {β : Type u_2} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [PartialOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulMono α β] {a₁ a₂ : α} {b₁ b₂ : β} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) :
a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂

Binary rearrangement inequality.

source
theorem smul_add_smul_le_smul_add_smul' {α : Type u_1} {β : Type u_2} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [PartialOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulMono α β] {a₁ a₂ : α} {b₁ b₂ : β} (ha : a₂ ≤ a₁) (hb : b₂ ≤ b₁) :
a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂

Binary rearrangement inequality.

source
theorem smul_add_smul_lt_smul_add_smul {α : Type u_1} {β : Type u_2} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [PartialOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulStrictMono α β] {a₁ a₂ : α} {b₁ b₂ : β} (ha : a₁ < a₂) (hb : b₁ < b₂) :
a₁ • b₂ + a₂ • b₁ < a₁ • b₁ + a₂ • b₂

Binary strict rearrangement inequality.

source
theorem smul_add_smul_lt_smul_add_smul' {α : Type u_1} {β : Type u_2} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [AddCommMonoid β] [PartialOrder β] [IsOrderedCancelAddMonoid β] [Module α β] [PosSMulStrictMono α β] {a₁ a₂ : α} {b₁ b₂ : β} (ha : a₂ < a₁) (hb : b₂ < b₁) :
a₁ • b₂ + a₂ • b₁ < a₁ • b₁ + a₂ • b₂

Binary strict rearrangement inequality.

source
theorem smul_le_smul_of_nonpos_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulMono α β] (h : b₁ ≤ b₂) (ha : a ≤ 0) :
a • b₂ ≤ a • b₁
source
theorem antitone_smul_left {α : Type u_1} {β : Type u_2} {a : α} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulMono α β] (ha : a ≤ 0) :
Antitone fun (x : β) => a • x
source
instance PosSMulMono.toSMulPosMono {α : Type u_1} {β : Type u_2} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulMono α β] :
SMulPosMono α β
source
theorem smul_lt_smul_of_neg_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] (hb : b₁ < b₂) (ha : a < 0) :
a • b₂ < a • b₁
source
theorem strictAnti_smul_left {α : Type u_1} {β : Type u_2} {a : α} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] (ha : a < 0) :
StrictAnti fun (x : β) => a • x
source
instance PosSMulStrictMono.toSMulPosStrictMono {α : Type u_1} {β : Type u_2} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] :
SMulPosStrictMono α β
source
theorem le_of_smul_le_smul_of_neg {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulReflectLE α β] (h : a • b₁ ≤ a • b₂) (ha : a < 0) :
b₂ ≤ b₁
source
theorem lt_of_smul_lt_smul_of_nonpos {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulReflectLT α β] (h : a • b₁ < a • b₂) (ha : a ≤ 0) :
b₂ < b₁
source
theorem smul_nonneg_of_nonpos_of_nonpos {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Ring α] [PartialOrder α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [SMulPosMono α β] (ha : a ≤ 0) (hb : b ≤ 0) :
0 ≤ a • b
source
theorem smul_le_smul_iff_of_neg_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulMono α β] [PosSMulReflectLE α β] (ha : a < 0) :
a • b₁ ≤ a • b₂ ↔ b₂ ≤ b₁
source
theorem smul_lt_smul_iff_of_neg_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : a < 0) :
a • b₁ < a • b₂ ↔ b₂ < b₁
source
theorem smul_pos_iff_of_neg_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : a < 0) :
0 < a • b ↔ b < 0
source
theorem smul_pos_of_neg_of_neg {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : a < 0) :
b < 0 → 0 < a • b

Alias of the reverse direction of `smul_pos_iff_of_neg_left`.

source
theorem smul_neg_iff_of_neg_left {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : a < 0) :
a • b < 0 ↔ 0 < b
source
theorem smul_max_of_nonpos {α : Type u_1} {β : Type u_2} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [LinearOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulMono α β] {a : α} (ha : a ≤ 0) (b₁ b₂ : β) :
a • max b₁ b₂ = min (a • b₁) (a • b₂)
source
theorem smul_min_of_nonpos {α : Type u_1} {β : Type u_2} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [LinearOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulMono α β] {a : α} (ha : a ≤ 0) (b₁ b₂ : β) :
a • min b₁ b₂ = max (a • b₁) (a • b₂)
source
theorem nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg {α : Type u_1} {β : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [AddCommGroup β] [LinearOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} (hab : 0 ≤ a • b) :
0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
source
theorem smul_nonneg_iff {α : Type u_1} {β : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [AddCommGroup β] [LinearOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} :
0 ≤ a • b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
source
theorem smul_nonpos_iff {α : Type u_1} {β : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [AddCommGroup β] [LinearOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} :
a • b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
source
theorem smul_nonneg_iff_pos_imp_nonneg {α : Type u_1} {β : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [AddCommGroup β] [LinearOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} :
0 ≤ a • b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)
source
theorem smul_nonneg_iff_neg_imp_nonpos {α : Type u_1} {β : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [AddCommGroup β] [LinearOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} :
0 ≤ a • b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
source
theorem smul_nonpos_iff_pos_imp_nonpos {α : Type u_1} {β : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [AddCommGroup β] [LinearOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} :
a • b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)
source
theorem smul_nonpos_iff_neg_imp_nonneg {α : Type u_1} {β : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [AddCommGroup β] [LinearOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} :
a • b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
source
instance Prod.instPosSMulMono {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero α] [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] [PosSMulMono α β] [PosSMulMono α γ] :
PosSMulMono α (β × γ)
source
instance Prod.instPosSMulReflectLE {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero α] [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] [PosSMulReflectLE α β] [PosSMulReflectLE α γ] :
PosSMulReflectLE α (β × γ)
source
instance Prod.instSMulPosMono {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] [Zero β] [Zero γ] [SMulPosMono α β] [SMulPosMono α γ] :
SMulPosMono α (β × γ)
source
instance Prod.instSMulPosReflectLE {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] [SMul α β] [SMul α γ] [Zero β] [Zero γ] [SMulPosReflectLE α β] [SMulPosReflectLE α γ] :
SMulPosReflectLE α (β × γ)
source
instance Prod.instPosSMulStrictMono {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero α] [PartialOrder α] [PartialOrder β] [PartialOrder γ] [Zero β] [Zero γ] [SMulWithZero α β] [SMulWithZero α γ] [PosSMulStrictMono α β] [PosSMulStrictMono α γ] :
PosSMulStrictMono α (β × γ)
source
instance Prod.instSMulPosStrictMono {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero α] [PartialOrder α] [PartialOrder β] [PartialOrder γ] [Zero β] [Zero γ] [SMulWithZero α β] [SMulWithZero α γ] [SMulPosStrictMono α β] [SMulPosStrictMono α γ] :
SMulPosStrictMono α (β × γ)
source
instance Prod.instSMulPosReflectLT {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero α] [PartialOrder α] [PartialOrder β] [PartialOrder γ] [Zero β] [Zero γ] [SMulWithZero α β] [SMulWithZero α γ] [SMulPosReflectLT α β] [SMulPosReflectLT α γ] :
SMulPosReflectLT α (β × γ)
source
instance Pi.instPosSMulMono {α : Type u_1} {ι : Type u_3} {β : ι → Type u_4} [Zero α] [Preorder α] [(i : ι) → Preorder (β i)] [(i : ι) → SMul α (β i)] [∀ (i : ι), PosSMulMono α (β i)] :
PosSMulMono α ((i : ι) → β i)
source
instance Pi.instPosSMulReflectLE {α : Type u_1} {ι : Type u_3} {β : ι → Type u_4} [Zero α] [Preorder α] [(i : ι) → Preorder (β i)] [(i : ι) → SMul α (β i)] [∀ (i : ι), PosSMulReflectLE α (β i)] :
PosSMulReflectLE α ((i : ι) → β i)
source
instance Pi.instSMulPosMono {α : Type u_1} {ι : Type u_3} {β : ι → Type u_4} [Preorder α] [(i : ι) → Preorder (β i)] [(i : ι) → SMul α (β i)] [(i : ι) → Zero (β i)] [∀ (i : ι), SMulPosMono α (β i)] :
SMulPosMono α ((i : ι) → β i)
source
instance Pi.instSMulPosReflectLE {α : Type u_1} {ι : Type u_3} {β : ι → Type u_4} [Preorder α] [(i : ι) → Preorder (β i)] [(i : ι) → SMul α (β i)] [(i : ι) → Zero (β i)] [∀ (i : ι), SMulPosReflectLE α (β i)] :
SMulPosReflectLE α ((i : ι) → β i)
source
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)
source
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)
source
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)
source
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 α β
source
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 α β
source
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 α β
source
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 α β
source
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 α β
source
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 α β
source
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 α β
source
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 α β
source
instance OrderedSemiring.toPosSMulMonoNat {α : Type u_1} [Semiring α] [PartialOrder α] [IsOrderedRing α] :
PosSMulMono ℕ α
source
instance OrderedSemiring.toSMulPosMonoNat {α : Type u_1} [Semiring α] [PartialOrder α] [IsOrderedRing α] :
SMulPosMono ℕ α
source
instance StrictOrderedSemiring.toPosSMulStrictMonoNat {α : Type u_1} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] :
PosSMulStrictMono ℕ α
source
instance StrictOrderedSemiring.toSMulPosStrictMonoNat {α : Type u_1} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] :
SMulPosStrictMono ℕ α