# Monotonicity of multiplication by positive elements #

This file defines typeclasses to reason about monotonicity of the operations

• b ↦ a * b, "left multiplication"
• a ↦ a * b, "right multiplication"

We use eight typeclasses to encode the various properties we care about for those two operations. These typeclasses are meant to be mostly internal to this file, to set up each lemma in the appropriate generality.

Less granular typeclasses like OrderedAddCommMonoid, LinearOrderedField 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, α is an orders which has a 0 and a 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 multiplication (b ↦ a * b):

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

We use the following four typeclasses to reason about right multiplication (a ↦ a * b):

• 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₂.

## Implications #

As α gets more and more structure, those typeclasses end up being equivalent. The commonly used implications are:

• When α is a partial order:
• PosMulStrictMono → PosMulMono
• MulPosStrictMono → MulPosMono
• PosMulReflectLE → PosMulReflectLT
• MulPosReflectLE → MulPosReflectLT
• When α is a linear order:
• PosMulStrictMono → PosMulReflectLE
• MulPosStrictMono → MulPosReflectLE .
• When the multiplication of α is commutative:
• PosMulMono → MulPosMono
• PosMulStrictMono → MulPosStrictMono
• PosMulReflectLE → MulPosReflectLE
• PosMulReflectLT → MulPosReflectLT

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

Local notation for the nonnegative elements of a type α. TODO: actually make local.

Equations
Instances For

Local notation for the positive elements of a type α. TODO: actually make local.

Equations
Instances For
@[inline, reducible]
abbrev PosMulMono (α : Type u_1) [Mul α] [Zero α] [] :

Typeclass for monotonicity of 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 OrderedSemiring.

Equations
• = CovariantClass { x : α // 0 x } α (fun (x : { x : α // 0 x }) (y : α) => x * y) fun (x x_1 : α) => x x_1
Instances For
@[inline, reducible]
abbrev MulPosMono (α : Type u_1) [Mul α] [Zero α] [] :

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.

Equations
• = CovariantClass { x : α // 0 x } α (fun (x : { x : α // 0 x }) (y : α) => y * x) fun (x x_1 : α) => x x_1
Instances For
@[inline, reducible]
abbrev PosMulStrictMono (α : Type u_1) [Mul α] [Zero α] [] :

Typeclass for strict monotonicity of 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 StrictOrderedSemiring.

Equations
• = CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => x * y) fun (x x_1 : α) => x < x_1
Instances For
@[inline, reducible]
abbrev MulPosStrictMono (α : Type u_1) [Mul α] [Zero α] [] :

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.

Equations
• = CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * x) fun (x x_1 : α) => x < x_1
Instances For
@[inline, reducible]
abbrev PosMulReflectLT (α : Type u_1) [Mul α] [Zero α] [] :

Typeclass for strict reverse monotonicity of 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 LinearOrderedSemiring.

Equations
Instances For
@[inline, reducible]
abbrev MulPosReflectLT (α : Type u_1) [Mul α] [Zero α] [] :

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.

Equations
Instances For
@[inline, reducible]
abbrev PosMulReflectLE (α : Type u_1) [Mul α] [Zero α] [] :

Typeclass for reverse monotonicity of 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 LinearOrderedSemiring.

Equations
• = ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => x * y) fun (x x_1 : α) => x x_1
Instances For
@[inline, reducible]
abbrev MulPosReflectLE (α : Type u_1) [Mul α] [Zero α] [] :

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.

Equations
• = ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * x) fun (x x_1 : α) => x x_1
Instances For
instance PosMulMono.to_covariantClass_pos_mul_le {α : Type u_1} [Mul α] [Zero α] [] [] :
CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => x * y) fun (x x_1 : α) => x x_1
Equations
• =
instance MulPosMono.to_covariantClass_pos_mul_le {α : Type u_1} [Mul α] [Zero α] [] [] :
CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * x) fun (x x_1 : α) => x x_1
Equations
• =
instance PosMulReflectLT.to_contravariantClass_pos_mul_lt {α : Type u_1} [Mul α] [Zero α] [] [] :
ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => x * y) fun (x x_1 : α) => x < x_1
Equations
• =
instance MulPosReflectLT.to_contravariantClass_pos_mul_lt {α : Type u_1} [Mul α] [Zero α] [] [] :
ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * x) fun (x x_1 : α) => x < x_1
Equations
• =
theorem mul_le_mul_of_nonneg_left {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [] [] (h : b c) (a0 : 0 a) :
a * b a * c
theorem mul_le_mul_of_nonneg_right {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [] [] (h : b c) (a0 : 0 a) :
b * a c * a
theorem mul_lt_mul_of_pos_left {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [] [] (bc : b < c) (a0 : 0 < a) :
a * b < a * c
theorem mul_lt_mul_of_pos_right {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [] [] (bc : b < c) (a0 : 0 < a) :
b * a < c * a
theorem lt_of_mul_lt_mul_left {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [] [] (h : a * b < a * c) (a0 : 0 a) :
b < c
theorem lt_of_mul_lt_mul_right {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [] [] (h : b * a < c * a) (a0 : 0 a) :
b < c
theorem le_of_mul_le_mul_left {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [] [] (bc : a * b a * c) (a0 : 0 < a) :
b c
theorem le_of_mul_le_mul_right {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [] [] (bc : b * a c * a) (a0 : 0 < a) :
b c
theorem lt_of_mul_lt_mul_of_nonneg_left {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [] [] (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} {a : α} {b : α} {c : α} [Mul α] [Zero α] [] [] (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} {a : α} {b : α} {c : α} [Mul α] [Zero α] [] [] (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} {a : α} {b : α} {c : α} [Mul α] [Zero α] [] [] (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} {a : α} {b : α} {c : α} [Mul α] [Zero α] [] [] [] (a0 : 0 < a) :
a * b < a * c b < c
@[simp]
theorem mul_lt_mul_right {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [] [] [] (a0 : 0 < a) :
b * a < c * a b < c
@[simp]
theorem mul_le_mul_left {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [] [] [] (a0 : 0 < a) :
a * b a * c b c
@[simp]
theorem mul_le_mul_right {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [] [] [] (a0 : 0 < a) :
b * a c * a b c
theorem mul_le_mul_iff_of_pos_left {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [] [] [] (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} {a : α} {b : α} {c : α} [Mul α] [Zero α] [] [] [] (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} {a : α} {b : α} {c : α} [Mul α] [Zero α] [] [] [] (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} {a : α} {b : α} {c : α} [Mul α] [Zero α] [] [] [] (a0 : 0 < a) :
b * a < c * a b < c

Alias of mul_lt_mul_right.

theorem mul_lt_mul_of_pos_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [] [] [] (h₁ : a b) (h₂ : c < d) (a0 : 0 < a) (d0 : 0 d) :
a * c < b * d
theorem mul_lt_mul_of_le_of_le' {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [] [] [] (h₁ : a b) (h₂ : c < d) (b0 : 0 < b) (c0 : 0 c) :
a * c < b * d
theorem mul_lt_mul_of_nonneg_of_pos {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [] [] [] (h₁ : a < b) (h₂ : c d) (a0 : 0 a) (d0 : 0 < d) :
a * c < b * d
theorem mul_lt_mul_of_le_of_lt' {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [] [] [] (h₁ : a < b) (h₂ : c d) (b0 : 0 b) (c0 : 0 < c) :
a * c < b * d
theorem mul_lt_mul_of_pos_of_pos {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [] [] [] (h₁ : a < b) (h₂ : c < d) (a0 : 0 < a) (d0 : 0 < d) :
a * c < b * d
theorem mul_lt_mul_of_lt_of_lt' {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [] [] [] (h₁ : a < b) (h₂ : c < d) (b0 : 0 < b) (c0 : 0 < c) :
a * c < b * d
theorem mul_lt_of_mul_lt_of_nonneg_left {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [] [] (h : a * b < c) (hdb : d b) (ha : 0 a) :
a * d < c
theorem lt_mul_of_lt_mul_of_nonneg_left {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [] [] (h : a < b * c) (hcd : c d) (hb : 0 b) :
a < b * d
theorem mul_lt_of_mul_lt_of_nonneg_right {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [] [] (h : a * b < c) (hda : d a) (hb : 0 b) :
d * b < c
theorem lt_mul_of_lt_mul_of_nonneg_right {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [] [] (h : a < b * c) (hbd : b d) (hc : 0 c) :
a < d * c
instance PosMulStrictMono.toPosMulReflectLE {α : Type u_1} [Mul α] [Zero α] [] [] :
Equations
• =
instance MulPosStrictMono.toMulPosReflectLE {α : Type u_1} [Mul α] [Zero α] [] [] :
Equations
• =
theorem PosMulReflectLE.toPosMulStrictMono {α : Type u_1} [Mul α] [Zero α] [] [] :
theorem MulPosReflectLE.toMulPosStrictMono {α : Type u_1} [Mul α] [Zero α] [] [] :
theorem posMulStrictMono_iff_posMulReflectLE {α : Type u_1} [Mul α] [Zero α] [] :
theorem mulPosStrictMono_iff_mulPosReflectLE {α : Type u_1} [Mul α] [Zero α] [] :
theorem PosMulReflectLT.toPosMulMono {α : Type u_1} [Mul α] [Zero α] [] [] :
theorem MulPosReflectLT.toMulPosMono {α : Type u_1} [Mul α] [Zero α] [] [] :
theorem PosMulMono.toPosMulReflectLT {α : Type u_1} [Mul α] [Zero α] [] [] :
theorem MulPosMono.toMulPosReflectLT {α : Type u_1} [Mul α] [Zero α] [] [] :
theorem posMulMono_iff_posMulReflectLT {α : Type u_1} [Mul α] [Zero α] [] :
theorem mulPosMono_iff_mulPosReflectLT {α : Type u_1} [Mul α] [Zero α] [] :
theorem Left.mul_pos {α : Type u_1} {a : α} {b : α} [] [] [] (ha : 0 < a) (hb : 0 < b) :
0 < a * b

Assumes left covariance.

theorem mul_pos {α : Type u_1} {a : α} {b : α} [] [] [] (ha : 0 < a) (hb : 0 < b) :
0 < a * b

Alias of Left.mul_pos.

Assumes left covariance.

theorem mul_neg_of_pos_of_neg {α : Type u_1} {a : α} {b : α} [] [] [] (ha : 0 < a) (hb : b < 0) :
a * b < 0
@[simp]
theorem mul_pos_iff_of_pos_left {α : Type u_1} {a : α} {b : α} [] [] [] [] (h : 0 < a) :
0 < a * b 0 < b
theorem Right.mul_pos {α : Type u_1} {a : α} {b : α} [] [] [] (ha : 0 < a) (hb : 0 < b) :
0 < a * b

Assumes right covariance.

theorem mul_neg_of_neg_of_pos {α : Type u_1} {a : α} {b : α} [] [] [] (ha : a < 0) (hb : 0 < b) :
a * b < 0
@[simp]
theorem mul_pos_iff_of_pos_right {α : Type u_1} {a : α} {b : α} [] [] [] [] (h : 0 < b) :
0 < a * b 0 < a
theorem Left.mul_nonneg {α : Type u_1} {a : α} {b : α} [] [] [] (ha : 0 a) (hb : 0 b) :
0 a * b

Assumes left covariance.

theorem mul_nonneg {α : Type u_1} {a : α} {b : α} [] [] [] (ha : 0 a) (hb : 0 b) :
0 a * b

Alias of Left.mul_nonneg.

Assumes left covariance.

theorem mul_nonpos_of_nonneg_of_nonpos {α : Type u_1} {a : α} {b : α} [] [] [] (ha : 0 a) (hb : b 0) :
a * b 0
theorem Right.mul_nonneg {α : Type u_1} {a : α} {b : α} [] [] [] (ha : 0 a) (hb : 0 b) :
0 a * b

Assumes right covariance.

theorem mul_nonpos_of_nonpos_of_nonneg {α : Type u_1} {a : α} {b : α} [] [] [] (ha : a 0) (hb : 0 b) :
a * b 0
theorem pos_of_mul_pos_right {α : Type u_1} {a : α} {b : α} [] [] [] (h : 0 < a * b) (ha : 0 a) :
0 < b
theorem pos_of_mul_pos_left {α : Type u_1} {a : α} {b : α} [] [] [] (h : 0 < a * b) (hb : 0 b) :
0 < a
theorem pos_iff_pos_of_mul_pos {α : Type u_1} {a : α} {b : α} [] [] [] [] (hab : 0 < a * b) :
0 < a 0 < b
theorem mul_le_mul_of_le_of_le {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [] [] [] [] (h₁ : a b) (h₂ : c d) (a0 : 0 a) (d0 : 0 d) :
a * c b * d
theorem mul_le_mul {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [] [] [] [] (h₁ : a b) (h₂ : c d) (c0 : 0 c) (b0 : 0 b) :
a * c b * d
theorem mul_self_le_mul_self {α : Type u_1} {a : α} {b : α} [] [] [] [] (ha : 0 a) (hab : a b) :
a * a b * b
theorem mul_le_of_mul_le_of_nonneg_left {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [] [] [] (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} {a : α} {b : α} {c : α} {d : α} [] [] [] (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} {a : α} {b : α} {c : α} {d : α} [] [] [] (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} {a : α} {b : α} {c : α} {d : α} [] [] [] (h : a b * c) (hle : b d) (c0 : 0 c) :
a d * c
theorem posMulMono_iff_covariant_pos {α : Type u_1} [] [] :
CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => x * y) fun (x x_1 : α) => x x_1
theorem mulPosMono_iff_covariant_pos {α : Type u_1} [] [] :
CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * x) fun (x x_1 : α) => x x_1
theorem posMulReflectLT_iff_contravariant_pos {α : Type u_1} [] [] :
ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => x * y) fun (x x_1 : α) => x < x_1
theorem mulPosReflectLT_iff_contravariant_pos {α : Type u_1} [] [] :
ContravariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * x) fun (x x_1 : α) => x < x_1
instance PosMulStrictMono.toPosMulMono {α : Type u_1} [] [] [] :
Equations
• =
instance MulPosStrictMono.toMulPosMono {α : Type u_1} [] [] [] :
Equations
• =
instance PosMulReflectLE.toPosMulReflectLT {α : Type u_1} [] [] [] :
Equations
• =
instance MulPosReflectLE.toMulPosReflectLT {α : Type u_1} [] [] [] :
Equations
• =
theorem mul_left_cancel_iff_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [] [] [] (a0 : 0 < a) :
a * b = a * c b = c
theorem mul_right_cancel_iff_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [] [] [] (b0 : 0 < b) :
a * b = c * b a = c
theorem mul_eq_mul_iff_eq_and_eq_of_pos {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [] [] [] [] (hab : a b) (hcd : c d) (a0 : 0 < a) (d0 : 0 < d) :
a * c = b * d a = b c = d
theorem mul_eq_mul_iff_eq_and_eq_of_pos' {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [] [] [] [] (hab : a b) (hcd : c d) (b0 : 0 < b) (c0 : 0 < c) :
a * c = b * d a = b c = d
theorem pos_and_pos_or_neg_and_neg_of_mul_pos {α : Type u_1} {a : α} {b : α} [] [] [] [] (hab : 0 < a * b) :
0 < a 0 < b a < 0 b < 0
theorem neg_of_mul_pos_right {α : Type u_1} {a : α} {b : α} [] [] [] [] (h : 0 < a * b) (ha : a 0) :
b < 0
theorem neg_of_mul_pos_left {α : Type u_1} {a : α} {b : α} [] [] [] [] (h : 0 < a * b) (ha : b 0) :
a < 0
theorem neg_iff_neg_of_mul_pos {α : Type u_1} {a : α} {b : α} [] [] [] [] (hab : 0 < a * b) :
a < 0 b < 0
theorem Left.neg_of_mul_neg_left {α : Type u_1} {a : α} {b : α} [] [] [] (h : a * b < 0) (h1 : 0 a) :
b < 0
theorem Right.neg_of_mul_neg_left {α : Type u_1} {a : α} {b : α} [] [] [] (h : a * b < 0) (h1 : 0 a) :
b < 0
theorem Left.neg_of_mul_neg_right {α : Type u_1} {a : α} {b : α} [] [] [] (h : a * b < 0) (h1 : 0 b) :
a < 0
theorem Right.neg_of_mul_neg_right {α : Type u_1} {a : α} {b : α} [] [] [] (h : a * b < 0) (h1 : 0 b) :
a < 0

Lemmas of the form a ≤ a * b ↔ 1 ≤ b and a * b ≤ a ↔ b ≤ 1, which assume left covariance.

@[simp]
theorem le_mul_iff_one_le_right {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] [] (a0 : 0 < a) :
a a * b 1 b
@[simp]
theorem lt_mul_iff_one_lt_right {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] [] (a0 : 0 < a) :
a < a * b 1 < b
@[simp]
theorem mul_le_iff_le_one_right {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] [] (a0 : 0 < a) :
a * b a b 1
@[simp]
theorem mul_lt_iff_lt_one_right {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] [] (a0 : 0 < a) :
a * b < a b < 1

Lemmas of the form a ≤ b * a ↔ 1 ≤ b and a * b ≤ b ↔ a ≤ 1, which assume right covariance.

@[simp]
theorem le_mul_iff_one_le_left {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] [] (a0 : 0 < a) :
a b * a 1 b
@[simp]
theorem lt_mul_iff_one_lt_left {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] [] (a0 : 0 < a) :
a < b * a 1 < b
@[simp]
theorem mul_le_iff_le_one_left {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] [] (b0 : 0 < b) :
a * b b a 1
@[simp]
theorem mul_lt_iff_lt_one_left {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] [] (b0 : 0 < b) :
a * b < b a < 1

Lemmas of the form 1 ≤ b → a ≤ a * b.

Variants with < 0 and ≤ 0 instead of 0 < and 0 ≤ appear in Mathlib/Algebra/Order/Ring/Defs (which imports this file) as they need additional results which are not yet available here.

theorem mul_le_of_le_one_left {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] (hb : 0 b) (h : a 1) :
a * b b
theorem le_mul_of_one_le_left {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] (hb : 0 b) (h : 1 a) :
b a * b
theorem mul_le_of_le_one_right {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] (ha : 0 a) (h : b 1) :
a * b a
theorem le_mul_of_one_le_right {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] (ha : 0 a) (h : 1 b) :
a a * b
theorem mul_lt_of_lt_one_left {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] (hb : 0 < b) (h : a < 1) :
a * b < b
theorem lt_mul_of_one_lt_left {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] (hb : 0 < b) (h : 1 < a) :
b < a * b
theorem mul_lt_of_lt_one_right {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] (ha : 0 < a) (h : b < 1) :
a * b < a
theorem lt_mul_of_one_lt_right {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] (ha : 0 < a) (h : 1 < b) :
a < a * b

Lemmas of the form b ≤ c → a ≤ 1 → b * a ≤ c.

theorem mul_le_of_le_of_le_one_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] (h : b c) (ha : a 1) (hb : 0 b) :
b * a c
theorem mul_lt_of_le_of_lt_one_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] (bc : b c) (ha : a < 1) (b0 : 0 < b) :
b * a < c
theorem mul_lt_of_lt_of_le_one_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] (h : b < c) (ha : a 1) (hb : 0 b) :
b * a < c
theorem Left.mul_le_one_of_le_of_le {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] (ha : a 1) (hb : b 1) (a0 : 0 a) :
a * b 1

Assumes left covariance.

theorem Left.mul_lt_of_le_of_lt_one_of_pos {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] (ha : a 1) (hb : b < 1) (a0 : 0 < a) :
a * b < 1

Assumes left covariance.

theorem Left.mul_lt_of_lt_of_le_one_of_nonneg {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] (ha : a < 1) (hb : b 1) (a0 : 0 a) :
a * b < 1

Assumes left covariance.

theorem mul_le_of_le_of_le_one' {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] [] (bc : b c) (ha : a 1) (a0 : 0 a) (c0 : 0 c) :
b * a c
theorem mul_lt_of_lt_of_le_one' {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] [] (bc : b < c) (ha : a 1) (a0 : 0 < a) (c0 : 0 c) :
b * a < c
theorem mul_lt_of_le_of_lt_one' {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] [] (bc : b c) (ha : a < 1) (a0 : 0 a) (c0 : 0 < c) :
b * a < c
theorem mul_lt_of_lt_of_lt_one_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] [] (bc : b < c) (ha : a 1) (a0 : 0 < a) (c0 : 0 c) :
b * a < c

Lemmas of the form b ≤ c → 1 ≤ a → b ≤ c * a.

theorem le_mul_of_le_of_one_le_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] (h : b c) (ha : 1 a) (hc : 0 c) :
b c * a
theorem lt_mul_of_le_of_one_lt_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] (bc : b c) (ha : 1 < a) (c0 : 0 < c) :
b < c * a
theorem lt_mul_of_lt_of_one_le_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] (h : b < c) (ha : 1 a) (hc : 0 c) :
b < c * a
theorem Left.one_le_mul_of_le_of_le {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] (ha : 1 a) (hb : 1 b) (a0 : 0 a) :
1 a * b

Assumes left covariance.

theorem Left.one_lt_mul_of_le_of_lt_of_pos {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] (ha : 1 a) (hb : 1 < b) (a0 : 0 < a) :
1 < a * b

Assumes left covariance.

theorem Left.lt_mul_of_lt_of_one_le_of_nonneg {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] (ha : 1 < a) (hb : 1 b) (a0 : 0 a) :
1 < a * b

Assumes left covariance.

theorem le_mul_of_le_of_one_le' {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] [] (bc : b c) (ha : 1 a) (a0 : 0 a) (b0 : 0 b) :
b c * a
theorem lt_mul_of_le_of_one_lt' {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] [] (bc : b c) (ha : 1 < a) (a0 : 0 a) (b0 : 0 < b) :
b < c * a
theorem lt_mul_of_lt_of_one_le' {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] [] (bc : b < c) (ha : 1 a) (a0 : 0 < a) (b0 : 0 b) :
b < c * a
theorem lt_mul_of_lt_of_one_lt_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] [] (bc : b < c) (ha : 1 < a) (a0 : 0 < a) (b0 : 0 < b) :
b < c * a

Lemmas of the form a ≤ 1 → b ≤ c → a * b ≤ c.

theorem mul_le_of_le_one_of_le_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] (ha : a 1) (h : b c) (hb : 0 b) :
a * b c
theorem mul_lt_of_lt_one_of_le_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] (ha : a < 1) (h : b c) (hb : 0 < b) :
a * b < c
theorem mul_lt_of_le_one_of_lt_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] (ha : a 1) (h : b < c) (hb : 0 b) :
a * b < c
theorem Right.mul_lt_one_of_lt_of_le_of_pos {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] (ha : a < 1) (hb : b 1) (b0 : 0 < b) :
a * b < 1

Assumes right covariance.

theorem Right.mul_lt_one_of_le_of_lt_of_nonneg {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] (ha : a 1) (hb : b < 1) (b0 : 0 b) :
a * b < 1

Assumes right covariance.

theorem mul_lt_of_lt_one_of_lt_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] [] (ha : a < 1) (bc : b < c) (a0 : 0 < a) (c0 : 0 < c) :
a * b < c
theorem Right.mul_le_one_of_le_of_le {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] (ha : a 1) (hb : b 1) (b0 : 0 b) :
a * b 1

Assumes right covariance.

theorem mul_le_of_le_one_of_le' {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] [] (ha : a 1) (bc : b c) (a0 : 0 a) (c0 : 0 c) :
a * b c
theorem mul_lt_of_lt_one_of_le' {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] [] (ha : a < 1) (bc : b c) (a0 : 0 a) (c0 : 0 < c) :
a * b < c
theorem mul_lt_of_le_one_of_lt' {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] [] (ha : a 1) (bc : b < c) (a0 : 0 < a) (c0 : 0 c) :
a * b < c

Lemmas of the form 1 ≤ a → b ≤ c → b ≤ a * c`.

theorem lt_mul_of_one_lt_of_le_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] (ha : 1 < a) (h : b c) (hc : 0 < c) :
b < a * c
theorem lt_mul_of_one_le_of_lt_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] (ha : 1 a) (h : b < c) (hc : 0 c) :
b < a * c
theorem lt_mul_of_one_lt_of_lt_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] (ha : 1 < a) (h : b < c) (hc : 0 < c) :
b < a * c
theorem Right.one_lt_mul_of_lt_of_le_of_pos {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] (ha : 1 < a) (hb : 1 b) (b0 : 0 < b) :
1 < a * b

Assumes right covariance.

theorem Right.one_lt_mul_of_le_of_lt_of_nonneg {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] (ha : 1 a) (hb : 1 < b) (b0 : 0 b) :
1 < a * b

Assumes right covariance.

theorem Right.one_lt_mul_of_lt_of_lt {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] (ha : 1 < a) (hb : 1 < b) (b0 : 0 < b) :
1 < a * b

Assumes right covariance.

theorem lt_mul_of_one_lt_of_lt_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] (ha : 1 a) (h : b < c) (hc : 0 c) :
b < a * c
theorem lt_of_mul_lt_of_one_le_of_nonneg_left {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] (h : a * b < c) (hle : 1 b) (ha : 0 a) :
a < c
theorem lt_of_lt_mul_of_le_one_of_nonneg_left {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] (h : a < b * c) (hc : c 1) (hb : 0 b) :
a < b
theorem lt_of_lt_mul_of_le_one_of_nonneg_right {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] (h : a < b * c) (hb : b 1) (hc : 0 c) :
a < c
theorem le_mul_of_one_le_of_le_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] (ha : 1 a) (bc : b c) (c0 : 0 c) :
b a * c
theorem Right.one_le_mul_of_le_of_le {α : Type u_1} {a : α} {b : α} [] [Zero α] [] [] (ha : 1 a) (hb : 1 b) (b0 : 0 b) :
1 a * b

Assumes right covariance.

theorem le_of_mul_le_of_one_le_of_nonneg_left {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] (h : a * b c) (hb : 1 b) (ha : 0 a) :
a c
theorem le_of_le_mul_of_le_one_of_nonneg_left {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] (h : a b * c) (hc : c 1) (hb : 0 b) :
a b
theorem le_of_mul_le_of_one_le_nonneg_right {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] (h : a * b c) (ha : 1 a) (hb : 0 b) :
b c
theorem le_of_le_mul_of_le_one_of_nonneg_right {α : Type u_1} {a : α} {b : α} {c : α} [] [Zero α] [] [] (h : a b * c) (hb : b 1) (hc : 0 c) :
a c
theorem exists_square_le' {α : Type u_1} {a : α} [] [Zero α] [] [] (a0 : 0 < a) :
∃ (b : α), b * b a
theorem PosMulMono.toPosMulStrictMono {α : Type u_1} [] [] :
theorem MulPosMono.toMulPosStrictMono {α : Type u_1} [] [] :
theorem posMulStrictMono_iff_mulPosStrictMono {α : Type u_1} [Mul α] [IsSymmOp α α fun (x x_1 : α) => x * x_1] [Zero α] [] :
theorem posMulReflectLT_iff_mulPosReflectLT {α : Type u_1} [Mul α] [IsSymmOp α α fun (x x_1 : α) => x * x_1] [Zero α] [] :
theorem posMulMono_iff_mulPosMono {α : Type u_1} [Mul α] [IsSymmOp α α fun (x x_1 : α) => x * x_1] [Zero α] [] :
theorem posMulReflectLE_iff_mulPosReflectLE {α : Type u_1} [Mul α] [IsSymmOp α α fun (x x_1 : α) => x * x_1] [Zero α] [] :