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

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

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

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

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

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

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

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

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

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

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

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

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

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 α] : PosMulMono α

@[instance 100]

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

@[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 α] : MulPosMono α

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 α] : PosMulMono α

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

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 α