# mathlib3documentation

algebra.order.ring.lemmas

# Multiplication by ·positive· elements is monotonic #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Let `α` be a type with `<` and `0`. We use the type `{x : α // 0 < x}` of positive elements of `α` to prove results about monotonicity of multiplication. We also introduce the local notation `α>0` for the subtype `{x : α // 0 < x}`:

If the type `α` also has a multiplication, then we combine this with (`contravariant_`) `covariant_class`es to assume that multiplication by positive elements is (strictly) monotone on a `mul_zero_class`, `monoid_with_zero`,... More specifically, we use extensively the following typeclasses:

• monotone left
• `covariant_class α>0 α (λ x y, x * y) (≤)`, abbreviated `pos_mul_mono α`, expressing that multiplication by positive elements on the left is monotone;
• `covariant_class α>0 α (λ x y, x * y) (<)`, abbreviated `pos_mul_strict_mono α`, expressing that multiplication by positive elements on the left is strictly monotone;
• monotone right
• `covariant_class α>0 α (λ x y, y * x) (≤)`, abbreviated `mul_pos_mono α`, expressing that multiplication by positive elements on the right is monotone;
• `covariant_class α>0 α (λ x y, y * x) (<)`, abbreviated `mul_pos_strict_mono α`, expressing that multiplication by positive elements on the right is strictly monotone.
• reverse monotone left
• `contravariant_class α>0 α (λ x y, x * y) (≤)`, abbreviated `pos_mul_mono_rev α`, expressing that multiplication by positive elements on the left is reverse monotone;
• `contravariant_class α>0 α (λ x y, x * y) (<)`, abbreviated `pos_mul_reflect_lt α`, expressing that multiplication by positive elements on the left is strictly reverse monotone;
• reverse reverse monotone right
• `contravariant_class α>0 α (λ x y, y * x) (≤)`, abbreviated `mul_pos_mono_rev α`, expressing that multiplication by positive elements on the right is reverse monotone;
• `contravariant_class α>0 α (λ x y, y * x) (<)`, abbreviated `mul_pos_reflect_lt α`, expressing that multiplication by positive elements on the right is strictly reverse monotone.

## Notation #

The following is local notation in this file:

• `α≥0`: `{x : α // 0 ≤ x}`
• `α>0`: `{x : α // 0 < x}`
@[reducible]
def pos_mul_mono (α : Type u_1) [has_mul α] [has_zero α] [preorder α] :
Prop

`pos_mul_mono α` is an abbreviation for `covariant_class α≥0 α (λ x y, x * y) (≤)`, expressing that multiplication by nonnegative elements on the left is monotone.

@[reducible]
def mul_pos_mono (α : Type u_1) [has_mul α] [has_zero α] [preorder α] :
Prop

`mul_pos_mono α` is an abbreviation for `covariant_class α≥0 α (λ x y, y * x) (≤)`, expressing that multiplication by nonnegative elements on the right is monotone.

@[reducible]
def pos_mul_strict_mono (α : Type u_1) [has_mul α] [has_zero α] [preorder α] :
Prop

`pos_mul_strict_mono α` is an abbreviation for `covariant_class α>0 α (λ x y, x * y) (<)`, expressing that multiplication by positive elements on the left is strictly monotone.

@[reducible]
def mul_pos_strict_mono (α : Type u_1) [has_mul α] [has_zero α] [preorder α] :
Prop

`mul_pos_strict_mono α` is an abbreviation for `covariant_class α>0 α (λ x y, y * x) (<)`, expressing that multiplication by positive elements on the right is strictly monotone.

@[reducible]
def pos_mul_reflect_lt (α : Type u_1) [has_mul α] [has_zero α] [preorder α] :
Prop

`pos_mul_reflect_lt α` is an abbreviation for `contravariant_class α≥0 α (λ x y, x * y) (<)`, expressing that multiplication by nonnegative elements on the left is strictly reverse monotone.

@[reducible]
def mul_pos_reflect_lt (α : Type u_1) [has_mul α] [has_zero α] [preorder α] :
Prop

`mul_pos_reflect_lt α` is an abbreviation for `contravariant_class α≥0 α (λ x y, y * x) (<)`, expressing that multiplication by nonnegative elements on the right is strictly reverse monotone.

@[reducible]
def pos_mul_mono_rev (α : Type u_1) [has_mul α] [has_zero α] [preorder α] :
Prop

`pos_mul_mono_rev α` is an abbreviation for `contravariant_class α>0 α (λ x y, x * y) (≤)`, expressing that multiplication by positive elements on the left is reverse monotone.

@[reducible]
def mul_pos_mono_rev (α : Type u_1) [has_mul α] [has_zero α] [preorder α] :
Prop

`mul_pos_mono_rev α` is an abbreviation for `contravariant_class α>0 α (λ x y, y * x) (≤)`, expressing that multiplication by positive elements on the right is reverse monotone.

@[protected, instance]
def pos_mul_mono.to_covariant_class_pos_mul_le {α : Type u_1} [has_mul α] [has_zero α] [preorder α] [pos_mul_mono α] :
covariant_class {x // 0 < x} α (λ (x : {x // 0 < x}) (y : α), x * y) has_le.le
@[protected, instance]
def mul_pos_mono.to_covariant_class_pos_mul_le {α : Type u_1} [has_mul α] [has_zero α] [preorder α] [mul_pos_mono α] :
covariant_class {x // 0 < x} α (λ (x : {x // 0 < x}) (y : α), y * x) has_le.le
@[protected, instance]
def pos_mul_reflect_lt.to_contravariant_class_pos_mul_lt {α : Type u_1} [has_mul α] [has_zero α] [preorder α]  :
contravariant_class {x // 0 < x} α (λ (x : {x // 0 < x}) (y : α), x * y) has_lt.lt
@[protected, instance]
def mul_pos_reflect_lt.to_contravariant_class_pos_mul_lt {α : Type u_1} [has_mul α] [has_zero α] [preorder α]  :
contravariant_class {x // 0 < x} α (λ (x : {x // 0 < x}) (y : α), y * x) has_lt.lt
theorem mul_le_mul_of_nonneg_left {α : Type u_1} {a b c : α} [has_mul α] [has_zero α] [preorder α] [pos_mul_mono α] (h : b c) (a0 : 0 a) :
a * b a * c
theorem mul_le_mul_of_nonneg_right {α : Type u_1} {a b c : α} [has_mul α] [has_zero α] [preorder α] [mul_pos_mono α] (h : b c) (a0 : 0 a) :
b * a c * a
theorem mul_lt_mul_of_pos_left {α : Type u_1} {a b c : α} [has_mul α] [has_zero α] [preorder α] (bc : b < c) (a0 : 0 < a) :
a * b < a * c
theorem mul_lt_mul_of_pos_right {α : Type u_1} {a b c : α} [has_mul α] [has_zero α] [preorder α] (bc : b < c) (a0 : 0 < a) :
b * a < c * a
theorem lt_of_mul_lt_mul_left {α : Type u_1} {a b c : α} [has_mul α] [has_zero α] [preorder α] (h : a * b < a * c) (a0 : 0 a) :
b < c
theorem lt_of_mul_lt_mul_right {α : Type u_1} {a b c : α} [has_mul α] [has_zero α] [preorder α] (h : b * a < c * a) (a0 : 0 a) :
b < c
theorem le_of_mul_le_mul_left {α : Type u_1} {a b c : α} [has_mul α] [has_zero α] [preorder α] (bc : a * b a * c) (a0 : 0 < a) :
b c
theorem le_of_mul_le_mul_right {α : Type u_1} {a b c : α} [has_mul α] [has_zero α] [preorder α] (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 : α} [has_mul α] [has_zero α] [preorder α] (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 : α} [has_mul α] [has_zero α] [preorder α] (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 : α} [has_mul α] [has_zero α] [preorder α] (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 : α} [has_mul α] [has_zero α] [preorder α] (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 : α} [has_mul α] [has_zero α] [preorder α] (a0 : 0 < a) :
a * b < a * c b < c
@[simp]
theorem mul_lt_mul_right {α : Type u_1} {a b c : α} [has_mul α] [has_zero α] [preorder α] (a0 : 0 < a) :
b * a < c * a b < c
@[simp]
theorem mul_le_mul_left {α : Type u_1} {a b c : α} [has_mul α] [has_zero α] [preorder α] [pos_mul_mono α] (a0 : 0 < a) :
a * b a * c b c
@[simp]
theorem mul_le_mul_right {α : Type u_1} {a b c : α} [has_mul α] [has_zero α] [preorder α] [mul_pos_mono α] (a0 : 0 < a) :
b * a c * a b c
theorem mul_lt_mul_of_pos_of_nonneg {α : Type u_1} {a b c d : α} [has_mul α] [has_zero α] [preorder α] [mul_pos_mono α] (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 : α} [has_mul α] [has_zero α] [preorder α] [mul_pos_mono α] (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 : α} [has_mul α] [has_zero α] [preorder α] [pos_mul_mono α] (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 : α} [has_mul α] [has_zero α] [preorder α] [pos_mul_mono α] (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 : α} [has_mul α] [has_zero α] [preorder α] (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 : α} [has_mul α] [has_zero α] [preorder α] (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 : α} [has_mul α] [has_zero α] [preorder α] [pos_mul_mono α] (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 : α} [has_mul α] [has_zero α] [preorder α] [pos_mul_mono α] (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 : α} [has_mul α] [has_zero α] [preorder α] [mul_pos_mono α] (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 : α} [has_mul α] [has_zero α] [preorder α] [mul_pos_mono α] (h : a < b * c) (hbd : b d) (hc : 0 c) :
a < d * c
@[protected, instance]
@[protected, instance]
theorem left.mul_pos {α : Type u_1} {a b : α} [preorder α] (ha : 0 < a) (hb : 0 < b) :
0 < a * b

Assumes left covariance.

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

Alias of `left.mul_pos`.

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

Assumes right covariance.

theorem mul_neg_of_neg_of_pos {α : Type u_1} {a b : α} [preorder α] (ha : a < 0) (hb : 0 < b) :
a * b < 0
@[simp]
theorem zero_lt_mul_right {α : Type u_1} {b c : α} [preorder α] (h : 0 < c) :
0 < b * c 0 < b
theorem left.mul_nonneg {α : Type u_1} {a b : α} [preorder α] [pos_mul_mono α] (ha : 0 a) (hb : 0 b) :
0 a * b

Assumes left covariance.

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

Alias of `left.mul_nonneg`.

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

Assumes right covariance.

theorem mul_nonpos_of_nonpos_of_nonneg {α : Type u_1} {a b : α} [preorder α] [mul_pos_mono α] (ha : a 0) (hb : 0 b) :
a * b 0
theorem pos_of_mul_pos_right {α : Type u_1} {a b : α} [preorder α] (h : 0 < a * b) (ha : 0 a) :
0 < b
theorem pos_of_mul_pos_left {α : Type u_1} {a b : α} [preorder α] (h : 0 < a * b) (hb : 0 b) :
0 < a
theorem pos_iff_pos_of_mul_pos {α : Type u_1} {a b : α} [preorder α] (hab : 0 < a * b) :
0 < a 0 < b
theorem mul_le_mul_of_le_of_le {α : Type u_1} {a b c d : α} [preorder α] [pos_mul_mono α] [mul_pos_mono α] (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 : α} [preorder α] [pos_mul_mono α] [mul_pos_mono α] (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 : α} [preorder α] [pos_mul_mono α] [mul_pos_mono α] (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 : α} [preorder α] [pos_mul_mono α] (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 : α} [preorder α] [pos_mul_mono α] (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 : α} [preorder α] [mul_pos_mono α] (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 : α} [preorder α] [mul_pos_mono α] (h : a b * c) (hle : b d) (c0 : 0 c) :
a d * c
theorem pos_mul_mono_iff_covariant_pos {α : Type u_1}  :
covariant_class {x // 0 < x} α (λ (x : {x // 0 < x}) (y : α), x * y) has_le.le
theorem mul_pos_mono_iff_covariant_pos {α : Type u_1}  :
covariant_class {x // 0 < x} α (λ (x : {x // 0 < x}) (y : α), y * x) has_le.le
theorem pos_mul_reflect_lt_iff_contravariant_pos {α : Type u_1}  :
contravariant_class {x // 0 < x} α (λ (x : {x // 0 < x}) (y : α), x * y) has_lt.lt
theorem mul_pos_reflect_lt_iff_contravariant_pos {α : Type u_1}  :
contravariant_class {x // 0 < x} α (λ (x : {x // 0 < x}) (y : α), y * x) has_lt.lt
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
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 : α} (hac : a b) (hbd : 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 : α} (hac : a b) (hbd : 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 : α} [linear_order α] [pos_mul_mono α] [mul_pos_mono α] (hab : 0 < a * b) :
0 < a 0 < b a < 0 b < 0
theorem neg_of_mul_pos_right {α : Type u_1} {a b : α} [linear_order α] [pos_mul_mono α] [mul_pos_mono α] (h : 0 < a * b) (ha : a 0) :
b < 0
theorem neg_of_mul_pos_left {α : Type u_1} {a b : α} [linear_order α] [pos_mul_mono α] [mul_pos_mono α] (h : 0 < a * b) (ha : b 0) :
a < 0
theorem neg_iff_neg_of_mul_pos {α : Type u_1} {a b : α} [linear_order α] [pos_mul_mono α] [mul_pos_mono α] (hab : 0 < a * b) :
a < 0 b < 0
theorem left.neg_of_mul_neg_left {α : Type u_1} {a b : α} [linear_order α] [pos_mul_mono α] (h : a * b < 0) (h1 : 0 a) :
b < 0
theorem right.neg_of_mul_neg_left {α : Type u_1} {a b : α} [linear_order α] [mul_pos_mono α] (h : a * b < 0) (h1 : 0 a) :
b < 0
theorem left.neg_of_mul_neg_right {α : Type u_1} {a b : α} [linear_order α] [pos_mul_mono α] (h : a * b < 0) (h1 : 0 b) :
a < 0
theorem right.neg_of_mul_neg_right {α : Type u_1} {a b : α} [linear_order α] [mul_pos_mono α] (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 : α} [has_zero α] [preorder α] [pos_mul_mono α] (a0 : 0 < a) :
a a * b 1 b
@[simp]
theorem lt_mul_iff_one_lt_right {α : Type u_1} {a b : α} [has_zero α] [preorder α] (a0 : 0 < a) :
a < a * b 1 < b
@[simp]
theorem mul_le_iff_le_one_right {α : Type u_1} {a b : α} [has_zero α] [preorder α] [pos_mul_mono α] (a0 : 0 < a) :
a * b a b 1
@[simp]
theorem mul_lt_iff_lt_one_right {α : Type u_1} {a b : α} [has_zero α] [preorder α] (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 : α} [has_zero α] [preorder α] [mul_pos_mono α] (a0 : 0 < a) :
a b * a 1 b
@[simp]
theorem lt_mul_iff_one_lt_left {α : Type u_1} {a b : α} [has_zero α] [preorder α] (a0 : 0 < a) :
a < b * a 1 < b
@[simp]
theorem mul_le_iff_le_one_left {α : Type u_1} {a b : α} [has_zero α] [preorder α] [mul_pos_mono α] (b0 : 0 < b) :
a * b b a 1
@[simp]
theorem mul_lt_iff_lt_one_left {α : Type u_1} {a b : α} [has_zero α] [preorder α] (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 `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 : α} [has_zero α] [preorder α] [mul_pos_mono α] (hb : 0 b) (h : a 1) :
a * b b
theorem le_mul_of_one_le_left {α : Type u_1} {a b : α} [has_zero α] [preorder α] [mul_pos_mono α] (hb : 0 b) (h : 1 a) :
b a * b
theorem mul_le_of_le_one_right {α : Type u_1} {a b : α} [has_zero α] [preorder α] [pos_mul_mono α] (ha : 0 a) (h : b 1) :
a * b a
theorem le_mul_of_one_le_right {α : Type u_1} {a b : α} [has_zero α] [preorder α] [pos_mul_mono α] (ha : 0 a) (h : 1 b) :
a a * b
theorem mul_lt_of_lt_one_left {α : Type u_1} {a b : α} [has_zero α] [preorder α] (hb : 0 < b) (h : a < 1) :
a * b < b
theorem lt_mul_of_one_lt_left {α : Type u_1} {a b : α} [has_zero α] [preorder α] (hb : 0 < b) (h : 1 < a) :
b < a * b
theorem mul_lt_of_lt_one_right {α : Type u_1} {a b : α} [has_zero α] [preorder α] (ha : 0 < a) (h : b < 1) :
a * b < a
theorem lt_mul_of_one_lt_right {α : Type u_1} {a b : α} [has_zero α] [preorder α] (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 : α} [has_zero α] [preorder α] [pos_mul_mono α] (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 : α} [has_zero α] [preorder α] (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 : α} [has_zero α] [preorder α] [pos_mul_mono α] (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 : α} [has_zero α] [preorder α] [pos_mul_mono α] (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 : α} [has_zero α] [preorder α] (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 : α} [has_zero α] [preorder α] [pos_mul_mono α] (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 : α} [has_zero α] [preorder α] [pos_mul_mono α] [mul_pos_mono α] (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 : α} [has_zero α] [preorder α] [pos_mul_mono α] (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 : α} [has_zero α] [preorder α] [mul_pos_mono α] (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 : α} [has_zero α] [preorder α] [pos_mul_mono α] (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 : α} [has_zero α] [preorder α] [pos_mul_mono α] (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 : α} [has_zero α] [preorder α] (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 : α} [has_zero α] [preorder α] [pos_mul_mono α] (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 : α} [has_zero α] [preorder α] [pos_mul_mono α] (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 : α} [has_zero α] [preorder α] (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 : α} [has_zero α] [preorder α] [pos_mul_mono α] (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 : α} [has_zero α] [preorder α] [pos_mul_mono α] [mul_pos_mono α] (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 : α} [has_zero α] [preorder α] [mul_pos_mono α] (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 : α} [has_zero α] [preorder α] [pos_mul_mono α] (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 : α} [has_zero α] [preorder α] (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 : α} [has_zero α] [preorder α] [mul_pos_mono α] (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 : α} [has_zero α] [preorder α] (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 : α} [has_zero α] [preorder α] [mul_pos_mono α] (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 : α} [has_zero α] [preorder α] (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 : α} [has_zero α] [preorder α] [mul_pos_mono α] (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 : α} [has_zero α] [preorder α] (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 : α} [has_zero α] [preorder α] [mul_pos_mono α] (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 : α} [has_zero α] [preorder α] [pos_mul_mono α] [mul_pos_mono α] (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 : α} [has_zero α] [preorder α] [pos_mul_mono α] (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 : α} [has_zero α] [preorder α] [mul_pos_mono α] (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 : α} [has_zero α] [preorder α] (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 : α} [has_zero α] [preorder α] [mul_pos_mono α] (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 : α} [has_zero α] [preorder α] (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 : α} [has_zero α] [preorder α] (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 : α} [has_zero α] [preorder α] [mul_pos_mono α] (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 : α} [has_zero α] [preorder α] (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 : α} [has_zero α] [preorder α] [mul_pos_mono α] (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 : α} [has_zero α] [preorder α] [pos_mul_mono α] (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 : α} [has_zero α] [preorder α] [pos_mul_mono α] (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 : α} [has_zero α] [preorder α] [mul_pos_mono α] (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 : α} [has_zero α] [preorder α] [mul_pos_mono α] (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 : α} [has_zero α] [preorder α] [mul_pos_mono α] (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 : α} [has_zero α] [preorder α] [pos_mul_mono α] (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 : α} [has_zero α] [preorder α] [pos_mul_mono α] (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 : α} [has_zero α] [preorder α] [mul_pos_mono α] (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 : α} [has_zero α] [preorder α] [mul_pos_mono α] (h : a b * c) (hb : b 1) (hc : 0 c) :
a c
theorem exists_square_le' {α : Type u_1} {a : α} [has_zero α] [linear_order α] (a0 : 0 < a) :
(b : α), b * b a
theorem pos_mul_mono_iff_mul_pos_mono {α : Type u_1} [has_zero α] [preorder α] :