# (Strict) monotonicity of multiplication by nonnegative (positive) elements #

This file defines eight typeclasses expressing monotonicity (strict monotonicity) of multiplication on the left or right by nonnegative (positive) elements in a preorder.

For left multiplication (`a ↦ b * a`) we define the following typeclasses:

- `PosMulMono`: If `b ≥ 0`, then `a₁ ≤ a₂ → b * a₁ ≤ b * a₂`.
- `PosMulStrictMono`: If `b > 0`, then `a₁ < a₂ → b * a₁ < b * a₂`.
- `PosMulReflectLT`: If `b ≥ 0`, then `b * a₁ < b * a₂ → a₁ < a₂`.
- `PosMulReflectLE`: If `b > 0`, then `b * a₁ ≤ b * a₂ → a₁ ≤ a₂`.

For right multiplication (`a ↦ a * b`) we define the following typeclasses:

- `MulPosMono`: If `b ≥ 0`, then `a₁ ≤ a₂ → a₁ * b ≤ a₂ * b`.
- `MulPosStrictMono`: If `b > 0`, then `a₁ < a₂ → a₁ * b < a₂ * b`.
- `MulPosReflectLT`: If `b ≥ 0`, then `a₁ * b < a₂ * b → a₁ < a₂`.
- `MulPosReflectLE`: If `b > 0`, then `a₁ * b ≤ a₂ * b → a₁ ≤ a₂`.

We then provide statements and instances about these typeclasses not requiring `MulZeroClass` or higher on the underlying type – those that do can be found in `Mathlib/Algebra/Order/GroupWithZero/Unbundled/Basic.lean`.

Less granular typeclasses like `OrderedAddCommMonoid` and `LinearOrderedField` should be enough for most purposes, and the system is set up so that they imply the correct granular typeclasses here.

## Implications #

As the underlying type `α` gets more structured, some of the above typeclasses become equivalent. The commonly used implications are:

- When `α` is a partial order (in `Mathlib/Algebra/Order/GroupWithZero/Unbundled/Basic.lean`):
  - `PosMulStrictMono.toPosMulMono`
  - `MulPosStrictMono.toMulPosMono`
  - `PosMulReflectLE.toPosMulReflectLT`
  - `MulPosReflectLE.toMulPosReflectLT`
- When `α` is a linear order:
  - `PosMulStrictMono.toPosMulReflectLE`
  - `MulPosStrictMono.toMulPosReflectLE`
- When multiplication on `α` is commutative:
  - `posMulMono_iff_mulPosMono`
  - `posMulStrictMono_iff_mulPosStrictMono`
  - `posMulReflectLE_iff_mulPosReflectLE`
  - `posMulReflectLT_iff_mulPosReflectLT`

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

- `OrderedSemiring → PosMulMono`
- `OrderedSemiring → MulPosMono`
- `StrictOrderedSemiring → PosMulStrictMono`
- `StrictOrderedSemiring → MulPosStrictMono`

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

## Notation #

The following is local notation in this file:

- `α≥0`: `{x : α // 0 ≤ x}`
- `α>0`: `{x : α // 0 < x}`

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/notation.20for.20positive.20elements for a discussion about this notation, and whether to enable it globally (note that the notation is currently global but broken, hence actually only works locally).

source
class PosMulMono (α : Type u_1) [Mul α] [Zero α] [Preorder α] :
Prop

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

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

- mul_le_mul_of_nonneg_left ⦃a : α⦄ (ha : 0 ≤ a) ⦃b c : α⦄ (hbc : b ≤ c) : a * b ≤ a * c

  Do not use this. Use `_root_.mul_le_mul_of_nonneg_left` instead.

Instances

source
theorem posMulMono_iff (α : Type u_1) [Mul α] [Zero α] [Preorder α] :
PosMulMono α ↔ ∀ ⦃a : α⦄, 0 ≤ a → ∀ ⦃b c : α⦄, b ≤ c → a * b ≤ a * c
source
class PosMulStrictMono (α : Type u_1) [Mul α] [Zero α] [Preorder α] :
Prop

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

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

- mul_lt_mul_of_pos_left ⦃a : α⦄ (ha : 0 < a) ⦃b c : α⦄ (hbc : b < c) : a * b < a * c

  Do not use this. Use `_root_.mul_lt_mul_of_pos_left` instead.

Instances

source
theorem posMulStrictMono_iff (α : Type u_1) [Mul α] [Zero α] [Preorder α] :
PosMulStrictMono α ↔ ∀ ⦃a : α⦄, 0 < a → ∀ ⦃b c : α⦄, b < c → a * b < a * c
source
class PosMulReflectLT (α : Type u_1) [Mul α] [Zero α] [Preorder α] extends ContravariantClass { x : α // 0 ≤ x } α (fun (x : { x : α // 0 ≤ x }) (y : α) => ↑x * y) fun (x1 x2 : α) => x1 < x2 :
Prop

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

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

- elim : Contravariant { x : α // 0 ≤ x } α (fun (x : { x : α // 0 ≤ x }) (y : α) => ↑x * y) fun (x1 x2 : α) => x1 < x2

Instances

source
theorem posMulReflectLT_iff (α : Type u_1) [Mul α] [Zero α] [Preorder α] :
PosMulReflectLT α ↔ ContravariantClass { x : α // 0 ≤ x } α (fun (x : { x : α // 0 ≤ x }) (y : α) => ↑x * y) fun (x1 x2 : α) => x1 < x2
source
class PosMulReflectLE (α : Type u_1) [Mul α] [Zero α] [Preorder α] extends ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => ↑x * y) fun (x1 x2 : α) => x1 ≤ x2 :
Prop

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

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

- elim : Contravariant { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => ↑x * y) fun (x1 x2 : α) => x1 ≤ x2

Instances

source
theorem posMulReflectLE_iff (α : Type u_1) [Mul α] [Zero α] [Preorder α] :
PosMulReflectLE α ↔ ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => ↑x * y) fun (x1 x2 : α) => x1 ≤ x2
source
class MulPosMono (α : Type u_1) [Mul α] [Zero α] [Preorder α] :
Prop

Typeclass for monotonicity of multiplication by nonnegative elements on the right, 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 `OrderedSemiring`.

- mul_le_mul_of_nonneg_right ⦃c : α⦄ (hc : 0 ≤ c) ⦃a b : α⦄ (hab : a ≤ b) : a * c ≤ b * c

  Do not use this. Use `_root_.mul_le_mul_of_nonneg_right` instead.

Instances

source
theorem mulPosMono_iff (α : Type u_1) [Mul α] [Zero α] [Preorder α] :
MulPosMono α ↔ ∀ ⦃c : α⦄, 0 ≤ c → ∀ ⦃a b : α⦄, a ≤ b → a * c ≤ b * c
source
class MulPosStrictMono (α : Type u_1) [Mul α] [Zero α] [Preorder α] :
Prop

Typeclass for strict monotonicity of multiplication by positive elements on the right, 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 `StrictOrderedSemiring`.

- mul_lt_mul_of_pos_right ⦃c : α⦄ (hc : 0 < c) ⦃a b : α⦄ (hab : a < b) : a * c < b * c

  Do not use this. Use `_root_.mul_lt_mul_of_pos_right` instead.

Instances

source
theorem mulPosStrictMono_iff (α : Type u_1) [Mul α] [Zero α] [Preorder α] :
MulPosStrictMono α ↔ ∀ ⦃c : α⦄, 0 < c → ∀ ⦃a b : α⦄, a < b → a * c < b * c
source
class MulPosReflectLT (α : Type u_1) [Mul α] [Zero α] [Preorder α] extends ContravariantClass { x : α // 0 ≤ x } α (fun (x : { x : α // 0 ≤ x }) (y : α) => y * ↑x) fun (x1 x2 : α) => x1 < x2 :
Prop

Typeclass for strict reverse monotonicity of multiplication by nonnegative elements on the right, 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 `LinearOrderedSemiring`.

- elim : Contravariant { x : α // 0 ≤ x } α (fun (x : { x : α // 0 ≤ x }) (y : α) => y * ↑x) fun (x1 x2 : α) => x1 < x2

Instances

source
theorem mulPosReflectLT_iff (α : Type u_1) [Mul α] [Zero α] [Preorder α] :
MulPosReflectLT α ↔ ContravariantClass { x : α // 0 ≤ x } α (fun (x : { x : α // 0 ≤ x }) (y : α) => y * ↑x) fun (x1 x2 : α) => x1 < x2
source
class MulPosReflectLE (α : Type u_1) [Mul α] [Zero α] [Preorder α] extends ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * ↑x) fun (x1 x2 : α) => x1 ≤ x2 :
Prop

Typeclass for reverse monotonicity of multiplication by positive elements on the right, 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 `LinearOrderedSemiring`.

- elim : Contravariant { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * ↑x) fun (x1 x2 : α) => x1 ≤ x2

Instances

source
theorem mulPosReflectLE_iff (α : Type u_1) [Mul α] [Zero α] [Preorder α] :
MulPosReflectLE α ↔ ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * ↑x) fun (x1 x2 : α) => x1 ≤ x2
source
instance PosMulMono.to_covariantClass_nonneg_mul_le {α : Type u_1} [Mul α] [Zero α] [Preorder α] [PosMulMono α] :
CovariantClass { x : α // 0 ≤ x } α (fun (x : { x : α // 0 ≤ x }) (y : α) => ↑x * y) fun (x1 x2 : α) => x1 ≤ x2
source
instance MulPosMono.to_covariantClass_nonneg_mul_le {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulPosMono α] :
CovariantClass { x : α // 0 ≤ x } α (fun (x : { x : α // 0 ≤ x }) (y : α) => y * ↑x) fun (x1 x2 : α) => x1 ≤ x2
source
instance PosMulMono.to_covariantClass_pos_mul_le {α : Type u_1} [Mul α] [Zero α] [Preorder α] [PosMulMono α] :
CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => ↑x * y) fun (x1 x2 : α) => x1 ≤ x2
source
instance MulPosMono.to_covariantClass_pos_mul_le {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulPosMono α] :
CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * ↑x) fun (x1 x2 : α) => x1 ≤ x2
source
instance PosMulStrictMono.to_covariantClass_pos_mul_le {α : Type u_1} [Mul α] [Zero α] [Preorder α] [PosMulStrictMono α] :
CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => ↑x * y) fun (x1 x2 : α) => x1 < x2
source
instance MulPosStrictMono.to_covariantClass_pos_mul_le {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulPosStrictMono α] :
CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * ↑x) fun (x1 x2 : α) => x1 < x2
source
instance PosMulReflectLT.to_contravariantClass_pos_mul_lt {α : Type u_1} [Mul α] [Zero α] [Preorder α] [PosMulReflectLT α] :
ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => ↑x * y) fun (x1 x2 : α) => x1 < x2
source
instance MulPosReflectLT.to_contravariantClass_pos_mul_lt {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulPosReflectLT α] :
ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * ↑x) fun (x1 x2 : α) => x1 < x2
source
@[instance 100]
instance MulLeftMono.toPosMulMono {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulLeftMono α] :
PosMulMono α
source
@[instance 100]
instance MulRightMono.toMulPosMono {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulRightMono α] :
MulPosMono α
source
@[instance 100]
instance MulLeftStrictMono.toPosMulStrictMono {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulLeftStrictMono α] :
PosMulStrictMono α
source
@[instance 100]
instance MulRightStrictMono.toMulPosStrictMono {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulRightStrictMono α] :
MulPosStrictMono α
source
@[instance 100]
instance MulLeftMono.toPosMulReflectLT {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulLeftReflectLT α] :
PosMulReflectLT α
source
@[instance 100]
instance MulRightMono.toMulPosReflectLT {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulRightReflectLT α] :
MulPosReflectLT α
source
@[instance 100]
instance MulLeftStrictMono.toPosMulReflectLE {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulLeftReflectLE α] :
PosMulReflectLE α
source
@[instance 100]
instance MulRightStrictMono.toMulPosReflectLE {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulRightReflectLE α] :
MulPosReflectLE α
source
theorem mul_le_mul_of_nonneg_left {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [PosMulMono α] (hbc : b ≤ c) (ha : 0 ≤ a) :
a * b ≤ a * c
source
theorem mul_le_mul_of_nonneg_right {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [MulPosMono α] (hbc : b ≤ c) (ha : 0 ≤ a) :
b * a ≤ c * a
source
theorem mul_lt_mul_of_pos_left {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [PosMulStrictMono α] (hbc : b < c) (ha : 0 < a) :
a * b < a * c
source
theorem mul_lt_mul_of_pos_right {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [MulPosStrictMono α] (hbc : b < c) (ha : 0 < a) :
b * a < c * a
source
theorem lt_of_mul_lt_mul_left {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [PosMulReflectLT α] (h : a * b < a * c) (a0 : 0 ≤ a) :
b < c
source
theorem lt_of_mul_lt_mul_right {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [MulPosReflectLT α] (h : b * a < c * a) (a0 : 0 ≤ a) :
b < c
source
theorem le_of_mul_le_mul_left {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [PosMulReflectLE α] (bc : a * b ≤ a * c) (a0 : 0 < a) :
b ≤ c
source
theorem le_of_mul_le_mul_right {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [MulPosReflectLE α] (bc : b * a ≤ c * a) (a0 : 0 < a) :
b ≤ c
source
theorem lt_of_mul_lt_mul_of_nonneg_left {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [PosMulReflectLT α] (h : a * b < a * c) (a0 : 0 ≤ a) :
b < c

Alias of `lt_of_mul_lt_mul_left`.

source
theorem lt_of_mul_lt_mul_of_nonneg_right {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [MulPosReflectLT α] (h : b * a < c * a) (a0 : 0 ≤ a) :
b < c

Alias of `lt_of_mul_lt_mul_right`.

source
theorem le_of_mul_le_mul_of_pos_left {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [PosMulReflectLE α] (bc : a * b ≤ a * c) (a0 : 0 < a) :
b ≤ c

Alias of `le_of_mul_le_mul_left`.

source
theorem le_of_mul_le_mul_of_pos_right {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [MulPosReflectLE α] (bc : b * a ≤ c * a) (a0 : 0 < a) :
b ≤ c

Alias of `le_of_mul_le_mul_right`.

source
theorem Function.Injective.posMulMono {α : Type u_1} [Mul α] [Zero α] [Preorder α] [PosMulMono α] {β : Type u_2} [Zero β] [Mul β] [Preorder β] (f : β → α) (zero : f 0 = 0) (mul : ∀ (x y : β), f (x * y) = f x * f y) (le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y) :
PosMulMono β

Pullback `PosMulMono`.

source
theorem Function.Injective.mulPosMono {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulPosMono α] {β : Type u_2} [Zero β] [Mul β] [Preorder β] (f : β → α) (zero : f 0 = 0) (mul : ∀ (x y : β), f (x * y) = f x * f y) (le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y) :
MulPosMono β

Pullback `MulPosMono`.

source
theorem Function.Injective.posMulStrictMono {α : Type u_1} [Mul α] [Zero α] [Preorder α] [PosMulStrictMono α] {β : Type u_2} [Zero β] [Mul β] [Preorder β] (f : β → α) (zero : f 0 = 0) (mul : ∀ (x y : β), f (x * y) = f x * f y) (lt : ∀ {x y : β}, f x < f y ↔ x < y) :
PosMulStrictMono β

Pullback `PosMulStrictMono`.

source
theorem Function.Injective.mulPosStrictMono {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulPosStrictMono α] {β : Type u_2} [Zero β] [Mul β] [Preorder β] (f : β → α) (zero : f 0 = 0) (mul : ∀ (x y : β), f (x * y) = f x * f y) (lt : ∀ {x y : β}, f x < f y ↔ x < y) :
MulPosStrictMono β

Pullback `MulPosStrictMono`.

source
@[simp]
theorem mul_lt_mul_iff_right₀ {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) :
a * b < a * c ↔ b < c
source
@[deprecated mul_lt_mul_iff_right₀ (since := "2025-09-25")]
theorem mul_lt_mul_left {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) :
a * b < a * c ↔ b < c

Alias of `mul_lt_mul_iff_right₀`.

source
@[simp]
theorem mul_lt_mul_iff_left₀ {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [MulPosStrictMono α] [MulPosReflectLT α] (a0 : 0 < a) :
b * a < c * a ↔ b < c
source
@[deprecated mul_lt_mul_iff_left₀ (since := "2025-09-25")]
theorem mul_lt_mul_right {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [MulPosStrictMono α] [MulPosReflectLT α] (a0 : 0 < a) :
b * a < c * a ↔ b < c

Alias of `mul_lt_mul_iff_left₀`.

source
@[simp]
theorem mul_le_mul_iff_right₀ {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [PosMulMono α] [PosMulReflectLE α] (a0 : 0 < a) :
a * b ≤ a * c ↔ b ≤ c
source
@[deprecated mul_le_mul_iff_right₀ (since := "2025-08-19")]
theorem mul_le_mul_left {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [PosMulMono α] [PosMulReflectLE α] (a0 : 0 < a) :
a * b ≤ a * c ↔ b ≤ c

Alias of `mul_le_mul_iff_right₀`.

source
@[simp]
theorem mul_le_mul_iff_left₀ {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [MulPosMono α] [MulPosReflectLE α] (a0 : 0 < a) :
b * a ≤ c * a ↔ b ≤ c
source
@[deprecated mul_le_mul_iff_left₀ (since := "2025-08-19")]
theorem mul_le_mul_right {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [MulPosMono α] [MulPosReflectLE α] (a0 : 0 < a) :
b * a ≤ c * a ↔ b ≤ c

Alias of `mul_le_mul_iff_left₀`.

source
theorem mul_le_mul_iff_of_pos_left {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [PosMulMono α] [PosMulReflectLE α] (a0 : 0 < a) :
a * b ≤ a * c ↔ b ≤ c

Alias of `mul_le_mul_iff_right₀`.

source
theorem mul_le_mul_iff_of_pos_right {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [MulPosMono α] [MulPosReflectLE α] (a0 : 0 < a) :
b * a ≤ c * a ↔ b ≤ c

Alias of `mul_le_mul_iff_left₀`.

source
theorem mul_lt_mul_iff_of_pos_left {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) :
a * b < a * c ↔ b < c

Alias of `mul_lt_mul_iff_right₀`.

source
theorem mul_lt_mul_iff_of_pos_right {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [MulPosStrictMono α] [MulPosReflectLT α] (a0 : 0 < a) :
b * a < c * a ↔ b < c

Alias of `mul_lt_mul_iff_left₀`.

source
theorem mul_le_mul_of_nonneg {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [PosMulMono α] [MulPosMono α] (h₁ : a ≤ b) (h₂ : c ≤ d) (a0 : 0 ≤ a) (d0 : 0 ≤ d) :
a * c ≤ b * d
source
theorem mul_le_mul_of_nonneg' {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [PosMulMono α] [MulPosMono α] (h₁ : a ≤ b) (h₂ : c ≤ d) (c0 : 0 ≤ c) (b0 : 0 ≤ b) :
a * c ≤ b * d
source
theorem mul_lt_mul_of_le_of_lt_of_pos_of_nonneg {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [PosMulStrictMono α] [MulPosMono α] (h₁ : a ≤ b) (h₂ : c < d) (a0 : 0 < a) (d0 : 0 ≤ d) :
a * c < b * d
source
theorem mul_lt_mul_of_pos_of_nonneg {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [PosMulStrictMono α] [MulPosMono α] (h₁ : a ≤ b) (h₂ : c < d) (a0 : 0 < a) (d0 : 0 ≤ d) :
a * c < b * d

Alias of `mul_lt_mul_of_le_of_lt_of_pos_of_nonneg`.

source
theorem mul_lt_mul_of_le_of_lt_of_nonneg_of_pos {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [PosMulStrictMono α] [MulPosMono α] (h₁ : a ≤ b) (h₂ : c < d) (c0 : 0 ≤ c) (b0 : 0 < b) :
a * c < b * d
source
theorem mul_lt_mul_of_nonneg_of_pos' {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [PosMulStrictMono α] [MulPosMono α] (h₁ : a ≤ b) (h₂ : c < d) (c0 : 0 ≤ c) (b0 : 0 < b) :
a * c < b * d

Alias of `mul_lt_mul_of_le_of_lt_of_nonneg_of_pos`.

source
theorem mul_lt_mul_of_lt_of_le_of_nonneg_of_pos {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [PosMulMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c ≤ d) (a0 : 0 ≤ a) (d0 : 0 < d) :
a * c < b * d
source
theorem mul_lt_mul_of_nonneg_of_pos {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [PosMulMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c ≤ d) (a0 : 0 ≤ a) (d0 : 0 < d) :
a * c < b * d

Alias of `mul_lt_mul_of_lt_of_le_of_nonneg_of_pos`.

source
theorem mul_lt_mul_of_lt_of_le_of_pos_of_nonneg {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [PosMulMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c ≤ d) (c0 : 0 < c) (b0 : 0 ≤ b) :
a * c < b * d
source
theorem mul_lt_mul_of_pos_of_nonneg' {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [PosMulMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c ≤ d) (c0 : 0 < c) (b0 : 0 ≤ b) :
a * c < b * d

Alias of `mul_lt_mul_of_lt_of_le_of_pos_of_nonneg`.

source
theorem mul_lt_mul_of_pos {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [PosMulStrictMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c < d) (a0 : 0 < a) (d0 : 0 < d) :
a * c < b * d
source
theorem mul_lt_mul_of_pos' {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [PosMulStrictMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c < d) (c0 : 0 < c) (b0 : 0 < b) :
a * c < b * d
source
theorem mul_le_mul {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [PosMulMono α] [MulPosMono α] (h₁ : a ≤ b) (h₂ : c ≤ d) (c0 : 0 ≤ c) (b0 : 0 ≤ b) :
a * c ≤ b * d

Alias of `mul_le_mul_of_nonneg'`.

source
theorem mul_lt_mul {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [PosMulMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c ≤ d) (c0 : 0 < c) (b0 : 0 ≤ b) :
a * c < b * d

Alias of `mul_lt_mul_of_lt_of_le_of_pos_of_nonneg`.

Alias of `mul_lt_mul_of_lt_of_le_of_pos_of_nonneg`.

source
theorem mul_lt_mul' {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [PosMulStrictMono α] [MulPosMono α] (h₁ : a ≤ b) (h₂ : c < d) (c0 : 0 ≤ c) (b0 : 0 < b) :
a * c < b * d

Alias of `mul_lt_mul_of_le_of_lt_of_nonneg_of_pos`.

Alias of `mul_lt_mul_of_le_of_lt_of_nonneg_of_pos`.

source
theorem mul_le_of_mul_le_of_nonneg_left {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [PosMulMono α] (h : a * b ≤ c) (hle : d ≤ b) (a0 : 0 ≤ a) :
a * d ≤ c
source
theorem mul_lt_of_mul_lt_of_nonneg_left {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [PosMulMono α] (h : a * b < c) (hle : d ≤ b) (a0 : 0 ≤ a) :
a * d < c
source
theorem le_mul_of_le_mul_of_nonneg_left {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [PosMulMono α] (h : a ≤ b * c) (hle : c ≤ d) (b0 : 0 ≤ b) :
a ≤ b * d
source
theorem lt_mul_of_lt_mul_of_nonneg_left {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [PosMulMono α] (h : a < b * c) (hle : c ≤ d) (b0 : 0 ≤ b) :
a < b * d
source
theorem mul_le_of_mul_le_of_nonneg_right {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [MulPosMono α] (h : a * b ≤ c) (hle : d ≤ a) (b0 : 0 ≤ b) :
d * b ≤ c
source
theorem mul_lt_of_mul_lt_of_nonneg_right {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [MulPosMono α] (h : a * b < c) (hle : d ≤ a) (b0 : 0 ≤ b) :
d * b < c
source
theorem le_mul_of_le_mul_of_nonneg_right {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [MulPosMono α] (h : a ≤ b * c) (hle : b ≤ d) (c0 : 0 ≤ c) :
a ≤ d * c
source
theorem lt_mul_of_lt_mul_of_nonneg_right {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c d : α} [MulPosMono α] (h : a < b * c) (hle : b ≤ d) (c0 : 0 ≤ c) :
a < d * c
source
theorem posMulMono_iff_mulPosMono {α : Type u_1} [Mul α] [Zero α] [Preorder α] [Std.Commutative fun (x1 x2 : α) => x1 * x2] :
PosMulMono α ↔ MulPosMono α
source
theorem PosMulMono.toMulPosMono {α : Type u_1} [Mul α] [Zero α] [Preorder α] [Std.Commutative fun (x1 x2 : α) => x1 * x2] [PosMulMono α] :
MulPosMono α
source
theorem posMulStrictMono_iff_mulPosStrictMono {α : Type u_1} [Mul α] [Zero α] [Preorder α] [Std.Commutative fun (x1 x2 : α) => x1 * x2] :
PosMulStrictMono α ↔ MulPosStrictMono α
source
theorem PosMulStrictMono.toMulPosStrictMono {α : Type u_1} [Mul α] [Zero α] [Preorder α] [Std.Commutative fun (x1 x2 : α) => x1 * x2] [PosMulStrictMono α] :
MulPosStrictMono α
source
theorem posMulReflectLE_iff_mulPosReflectLE {α : Type u_1} [Mul α] [Zero α] [Preorder α] [Std.Commutative fun (x1 x2 : α) => x1 * x2] :
PosMulReflectLE α ↔ MulPosReflectLE α
source
theorem PosMulReflectLE.toMulPosReflectLE {α : Type u_1} [Mul α] [Zero α] [Preorder α] [Std.Commutative fun (x1 x2 : α) => x1 * x2] [PosMulReflectLE α] :
MulPosReflectLE α
source
theorem posMulReflectLT_iff_mulPosReflectLT {α : Type u_1} [Mul α] [Zero α] [Preorder α] [Std.Commutative fun (x1 x2 : α) => x1 * x2] :
PosMulReflectLT α ↔ MulPosReflectLT α
source
theorem PosMulReflectLT.toMulPosReflectLT {α : Type u_1} [Mul α] [Zero α] [Preorder α] [Std.Commutative fun (x1 x2 : α) => x1 * x2] [PosMulReflectLT α] :
MulPosReflectLT α
source
@[instance 100]
instance PosMulStrictMono.toPosMulReflectLE {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] [PosMulStrictMono α] :
PosMulReflectLE α
source
@[instance 100]
instance MulPosStrictMono.toMulPosReflectLE {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] [MulPosStrictMono α] :
MulPosReflectLE α
source
theorem PosMulReflectLE.toPosMulStrictMono {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] [PosMulReflectLE α] :
PosMulStrictMono α
source
theorem MulPosReflectLE.toMulPosStrictMono {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] [MulPosReflectLE α] :
MulPosStrictMono α
source
theorem posMulStrictMono_iff_posMulReflectLE {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] :
PosMulStrictMono α ↔ PosMulReflectLE α
source
theorem mulPosStrictMono_iff_mulPosReflectLE {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] :
MulPosStrictMono α ↔ MulPosReflectLE α
source
theorem PosMulReflectLT.toPosMulMono {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] [PosMulReflectLT α] :
PosMulMono α
source
theorem MulPosReflectLT.toMulPosMono {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] [MulPosReflectLT α] :
MulPosMono α
source
theorem PosMulMono.toPosMulReflectLT {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] [PosMulMono α] :
PosMulReflectLT α
source
theorem MulPosMono.toMulPosReflectLT {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] [MulPosMono α] :
MulPosReflectLT α
source
theorem posMulMono_iff_posMulReflectLT {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] :
PosMulMono α ↔ PosMulReflectLT α
source
theorem mulPosMono_iff_mulPosReflectLT {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] :
MulPosMono α ↔ MulPosReflectLT α