Documentation

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs

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

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).

class PosMulMono (α : Type u_1) [Mul α] [Zero α] [Preorder α] extends CovariantClass { x : α // 0 ≤ x } α (fun (x : { x : α // 0 ≤ x }) (y : α) => ↑x * y) fun (x1 x2 : α) => x1 ≤ x2 :

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.

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

Instances

theorem posMulMono_iff (α : Type u_1) [Mul α] [Zero α] [Preorder α] :

PosMulMono α ↔ CovariantClass { x : α // 0 ≤ x } α (fun (x : { x : α // 0 ≤ x }) (y : α) => ↑x * y) fun (x1 x2 : α) => x1 ≤ x2

class PosMulStrictMono (α : Type u_1) [Mul α] [Zero α] [Preorder α] extends CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => ↑x * y) fun (x1 x2 : α) => x1 < x2 :

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.

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

Instances

theorem posMulStrictMono_iff (α : Type u_1) [Mul α] [Zero α] [Preorder α] :

PosMulStrictMono α ↔ CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => ↑x * y) fun (x1 x2 : α) => x1 < x2

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 :

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

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

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 :

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

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

class MulPosMono (α : Type u_1) [Mul α] [Zero α] [Preorder α] extends CovariantClass { x : α // 0 ≤ x } α (fun (x : { x : α // 0 ≤ x }) (y : α) => y * ↑x) fun (x1 x2 : α) => x1 ≤ x2 :

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.

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

Instances

theorem mulPosMono_iff (α : Type u_1) [Mul α] [Zero α] [Preorder α] :

MulPosMono α ↔ CovariantClass { x : α // 0 ≤ x } α (fun (x : { x : α // 0 ≤ x }) (y : α) => y * ↑x) fun (x1 x2 : α) => x1 ≤ x2

class MulPosStrictMono (α : Type u_1) [Mul α] [Zero α] [Preorder α] extends CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * ↑x) fun (x1 x2 : α) => x1 < x2 :

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.

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

Instances

theorem mulPosStrictMono_iff (α : Type u_1) [Mul α] [Zero α] [Preorder α] :

MulPosStrictMono α ↔ CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * ↑x) fun (x1 x2 : α) => x1 < x2

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 :

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

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

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 :

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

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

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

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

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

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

@[instance 100]

instance MulLeftMono.toPosMulMono {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulLeftMono α] :

@[instance 100]

instance MulRightMono.toMulPosMono {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulRightMono α] :

@[instance 100]

instance MulLeftStrictMono.toPosMulStrictMono {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulLeftStrictMono α] :

PosMulStrictMono α

@[instance 100]

instance MulRightStrictMono.toMulPosStrictMono {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulRightStrictMono α] :

MulPosStrictMono α

@[instance 100]

instance MulLeftMono.toPosMulReflectLT {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulLeftReflectLT α] :

PosMulReflectLT α

@[instance 100]

instance MulRightMono.toMulPosReflectLT {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulRightReflectLT α] :

MulPosReflectLT α

@[instance 100]

instance MulLeftStrictMono.toPosMulReflectLE {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulLeftReflectLE α] :

PosMulReflectLE α

@[instance 100]

instance MulRightStrictMono.toMulPosReflectLE {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulRightReflectLE α] :

MulPosReflectLE α

theorem mul_le_mul_of_nonneg_left {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [PosMulMono α] (h : b ≤ c) (a0 : 0 ≤ a) :

a * b ≤ a * c

theorem mul_le_mul_of_nonneg_right {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [MulPosMono α] (h : b ≤ c) (a0 : 0 ≤ a) :

b * a ≤ c * a

theorem mul_lt_mul_of_pos_left {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [PosMulStrictMono α] (bc : b < c) (a0 : 0 < a) :

a * b < a * c

theorem mul_lt_mul_of_pos_right {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [MulPosStrictMono α] (bc : b < c) (a0 : 0 < a) :

b * a < c * a

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

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

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

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

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.

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.

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.

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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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_left.

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_right.

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_left.

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_right.

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

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

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

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.

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

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.

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

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.

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

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.

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

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

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'.

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.

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.

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

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

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

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

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

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

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

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

theorem posMulMono_iff_mulPosMono {α : Type u_1} [Mul α] [Zero α] [Preorder α] [Std.Commutative fun (x1 x2 : α) => x1 * x2] :

PosMulMono α ↔ MulPosMono α

theorem PosMulMono.toMulPosMono {α : Type u_1} [Mul α] [Zero α] [Preorder α] [Std.Commutative fun (x1 x2 : α) => x1 * x2] [PosMulMono α] :

theorem posMulStrictMono_iff_mulPosStrictMono {α : Type u_1} [Mul α] [Zero α] [Preorder α] [Std.Commutative fun (x1 x2 : α) => x1 * x2] :

PosMulStrictMono α ↔ MulPosStrictMono α

theorem PosMulStrictMono.toMulPosStrictMono {α : Type u_1} [Mul α] [Zero α] [Preorder α] [Std.Commutative fun (x1 x2 : α) => x1 * x2] [PosMulStrictMono α] :

MulPosStrictMono α

theorem posMulReflectLE_iff_mulPosReflectLE {α : Type u_1} [Mul α] [Zero α] [Preorder α] [Std.Commutative fun (x1 x2 : α) => x1 * x2] :

PosMulReflectLE α ↔ MulPosReflectLE α

theorem PosMulReflectLE.toMulPosReflectLE {α : Type u_1} [Mul α] [Zero α] [Preorder α] [Std.Commutative fun (x1 x2 : α) => x1 * x2] [PosMulReflectLE α] :

MulPosReflectLE α

theorem posMulReflectLT_iff_mulPosReflectLT {α : Type u_1} [Mul α] [Zero α] [Preorder α] [Std.Commutative fun (x1 x2 : α) => x1 * x2] :

PosMulReflectLT α ↔ MulPosReflectLT α

theorem PosMulReflectLT.toMulPosReflectLT {α : Type u_1} [Mul α] [Zero α] [Preorder α] [Std.Commutative fun (x1 x2 : α) => x1 * x2] [PosMulReflectLT α] :

MulPosReflectLT α

@[instance 100]

instance PosMulStrictMono.toPosMulReflectLE {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] [PosMulStrictMono α] :

PosMulReflectLE α

@[instance 100]

instance MulPosStrictMono.toMulPosReflectLE {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] [MulPosStrictMono α] :

MulPosReflectLE α

theorem PosMulReflectLE.toPosMulStrictMono {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] [PosMulReflectLE α] :

PosMulStrictMono α

theorem MulPosReflectLE.toMulPosStrictMono {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] [MulPosReflectLE α] :

MulPosStrictMono α

theorem posMulStrictMono_iff_posMulReflectLE {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] :

PosMulStrictMono α ↔ PosMulReflectLE α

theorem mulPosStrictMono_iff_mulPosReflectLE {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] :

MulPosStrictMono α ↔ MulPosReflectLE α

theorem PosMulReflectLT.toPosMulMono {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] [PosMulReflectLT α] :

theorem MulPosReflectLT.toMulPosMono {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] [MulPosReflectLT α] :

theorem PosMulMono.toPosMulReflectLT {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] [PosMulMono α] :

PosMulReflectLT α

theorem MulPosMono.toMulPosReflectLT {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] [MulPosMono α] :

MulPosReflectLT α

theorem posMulMono_iff_posMulReflectLT {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] :

PosMulMono α ↔ PosMulReflectLT α

theorem mulPosMono_iff_mulPosReflectLT {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] :

MulPosMono α ↔ MulPosReflectLT α