Multiplication by ·positive· elements is monotonic

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) CovariantClasses to assume that multiplication by positive elements is (strictly) monotone on a MulZeroClass, MonoidWithZero,... More specifically, we use extensively the following typeclasses:

• monotone left
• • CovariantClass α>0 α (fun x y ↦ x * y) (≤), abbreviated PosMulMono α, expressing that multiplication by positive elements on the left is monotone;
• • CovariantClass α>0 α (fun x y ↦ x * y) (<), abbreviated PosMulStrictMono α, expressing that multiplication by positive elements on the left is strictly monotone;
• monotone right
• • CovariantClass α>0 α (fun x y ↦ y * x) (≤), abbreviated MulPosMono α, expressing that multiplication by positive elements on the right is monotone;
• • CovariantClass α>0 α (fun x y ↦ y * x) (<), abbreviated MulPosStrictMono α, expressing that multiplication by positive elements on the right is strictly monotone.
• reverse monotone left
• • ContravariantClass α>0 α (fun x y ↦ x * y) (≤), abbreviated PosMulMonoRev α, expressing that multiplication by positive elements on the left is reverse monotone;
• • ContravariantClass α>0 α (fun x y ↦ x * y) (<), abbreviated PosMulReflectLT α, expressing that multiplication by positive elements on the left is strictly reverse monotone;
• reverse reverse monotone right
• • ContravariantClass α>0 α (fun x y ↦ y * x) (≤), abbreviated MulPosMonoRev α, expressing that multiplication by positive elements on the right is reverse monotone;
• • ContravariantClass α>0 α (fun x y ↦ y * x) (<), abbreviated MulPosReflectLT α, 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}

def «termα≥0» : Lean.ParserDescr

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

def «termα>0» : Lean.ParserDescr

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

@[inline, reducible]

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

PosMulMono α is an abbreviation for CovariantClass α≥0 α (fun x y ↦ x * y) (≤), expressing that multiplication by nonnegative elements on the left is monotone.

@[inline, reducible]

abbrev MulPosMono (α : Type u_1) [Mul α] [Zero α] [Preorder α] : Prop

MulPosMono α is an abbreviation for CovariantClass α≥0 α (fun x y ↦ y * x) (≤), expressing that multiplication by nonnegative elements on the right is monotone.

@[inline, reducible]

abbrev PosMulStrictMono (α : Type u_1) [Mul α] [Zero α] [Preorder α] : Prop

PosMulStrictMono α is an abbreviation for CovariantClass α>0 α (fun x y ↦ x * y) (<), expressing that multiplication by positive elements on the left is strictly monotone.

@[inline, reducible]

abbrev MulPosStrictMono (α : Type u_1) [Mul α] [Zero α] [Preorder α] : Prop

MulPosStrictMono α is an abbreviation for CovariantClass α>0 α (fun x y ↦ y * x) (<), expressing that multiplication by positive elements on the right is strictly monotone.

@[inline, reducible]

abbrev PosMulReflectLT (α : Type u_1) [Mul α] [Zero α] [Preorder α] : Prop

PosMulReflectLT α is an abbreviation for ContravariantClas α≥0 α (fun x y ↦ x * y) (<), expressing that multiplication by nonnegative elements on the left is strictly reverse monotone.

@[inline, reducible]

abbrev MulPosReflectLT (α : Type u_1) [Mul α] [Zero α] [Preorder α] : Prop

MulPosReflectLT α is an abbreviation for ContravariantClas α≥0 α (fun x y ↦ y * x) (<), expressing that multiplication by nonnegative elements on the right is strictly reverse monotone.

@[inline, reducible]

abbrev PosMulMonoRev (α : Type u_1) [Mul α] [Zero α] [Preorder α] : Prop

PosMulMonoRev α is an abbreviation for ContravariantClas α>0 α (fun x y ↦ x * y) (≤), expressing that multiplication by positive elements on the left is reverse monotone.

@[inline, reducible]

abbrev MulPosMonoRev (α : Type u_1) [Mul α] [Zero α] [Preorder α] : Prop

MulPosMonoRev α is an abbreviation for ContravariantClas α>0 α (fun x y ↦ y * x) (≤), expressing that multiplication by positive elements on the right is reverse monotone.

instance PosMulMono.to_covariantClass_pos_mul_le {α : Type u_1} [Mul α] [Zero α] [Preorder α] [PosMulMono α] : CovariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x x_1 => x ≤ x_1

instance MulPosMono.to_covariantClass_pos_mul_le {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulPosMono α] : CovariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x x_1 => x ≤ x_1

instance PosMulReflectLT.to_contravariantClass_pos_mul_lt {α : Type u_1} [Mul α] [Zero α] [Preorder α] [PosMulReflectLT α] : ContravariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x x_1 => x < x_1

instance MulPosReflectLT.to_contravariantClass_pos_mul_lt {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulPosReflectLT α] : ContravariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x x_1 => x < x_1

theorem mul_le_mul_of_nonneg_left {α : Type u_1} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [PosMulMono α] (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 α] [Preorder α] [MulPosMono α] (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 α] [Preorder α] [PosMulStrictMono α] (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 α] [Preorder α] [MulPosStrictMono α] (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 α] [Preorder α] [PosMulReflectLT α] (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 α] [Preorder α] [MulPosReflectLT α] (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 α] [Preorder α] [PosMulMonoRev α] (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 α] [Preorder α] [MulPosMonoRev α] (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 α] [Preorder α] [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} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [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} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [PosMulMonoRev α] (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 α] [Preorder α] [MulPosMonoRev α] (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 α] [Preorder α] [PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) : a * b < a * c ↔ b < c

@[simp]

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

@[simp]

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

@[simp]

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

theorem mul_lt_mul_of_pos_of_nonneg {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [Mul α] [Zero α] [Preorder α] [PosMulStrictMono α] [MulPosMono α] (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 α] [Preorder α] [PosMulStrictMono α] [MulPosMono α] (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 α] [Preorder α] [PosMulMono α] [MulPosStrictMono α] (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 α] [Preorder α] [PosMulMono α] [MulPosStrictMono α] (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 α] [Preorder α] [PosMulStrictMono α] [MulPosStrictMono α] (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 α] [Preorder α] [PosMulStrictMono α] [MulPosStrictMono α] (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 α] [Preorder α] [PosMulMono α] (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 α] [Preorder α] [PosMulMono α] (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 α] [Preorder α] [MulPosMono α] (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 α] [Preorder α] [MulPosMono α] (h : a < b * c) (hbd : b ≤ d) (hc : 0 ≤ c) : a < d * c

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

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

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

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

theorem posMulStrictMono_iff_posMulMonoRev {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] : PosMulStrictMono α ↔ PosMulMonoRev α

theorem mulPosStrictMono_iff_mulPosMonoRev {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] : MulPosStrictMono α ↔ MulPosMonoRev α

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 α

theorem Left.mul_pos {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [PosMulStrictMono α] (ha : 0 < a) (hb : 0 < b) : 0 < a * b

Assumes left covariance.

theorem mul_pos {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [PosMulStrictMono α] (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 : α} [MulZeroClass α] [Preorder α] [PosMulStrictMono α] (ha : 0 < a) (hb : b < 0) : a * b < 0

@[simp]

theorem zero_lt_mul_left {α : Type u_1} {b : α} {c : α} [MulZeroClass α] [Preorder α] [PosMulStrictMono α] [PosMulReflectLT α] (h : 0 < c) : 0 < c * b ↔ 0 < b

theorem Right.mul_pos {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [MulPosStrictMono α] (ha : 0 < a) (hb : 0 < b) : 0 < a * b

Assumes right covariance.

theorem mul_neg_of_neg_of_pos {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [MulPosStrictMono α] (ha : a < 0) (hb : 0 < b) : a * b < 0

@[simp]

theorem zero_lt_mul_right {α : Type u_1} {b : α} {c : α} [MulZeroClass α] [Preorder α] [MulPosStrictMono α] [MulPosReflectLT α] (h : 0 < c) : 0 < b * c ↔ 0 < b

theorem Left.mul_nonneg {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [PosMulMono α] (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b

Assumes left covariance.

theorem mul_nonneg {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [PosMulMono α] (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 : α} [MulZeroClass α] [Preorder α] [PosMulMono α] (ha : 0 ≤ a) (hb : b ≤ 0) : a * b ≤ 0

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

Assumes right covariance.

theorem mul_nonpos_of_nonpos_of_nonneg {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [MulPosMono α] (ha : a ≤ 0) (hb : 0 ≤ b) : a * b ≤ 0

theorem pos_of_mul_pos_right {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [PosMulReflectLT α] (h : 0 < a * b) (ha : 0 ≤ a) : 0 < b

theorem pos_of_mul_pos_left {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [MulPosReflectLT α] (h : 0 < a * b) (hb : 0 ≤ b) : 0 < a

theorem pos_iff_pos_of_mul_pos {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [PosMulReflectLT α] [MulPosReflectLT α] (hab : 0 < a * b) : 0 < a ↔ 0 < b

theorem mul_le_mul_of_le_of_le {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [MulZeroClass α] [Preorder α] [PosMulMono α] [MulPosMono α] (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 : α} [MulZeroClass α] [Preorder α] [PosMulMono α] [MulPosMono α] (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 : α} [MulZeroClass α] [Preorder α] [PosMulMono α] [MulPosMono α] (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 : α} [MulZeroClass α] [Preorder α] [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} {a : α} {b : α} {c : α} {d : α} [MulZeroClass α] [Preorder α] [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} {a : α} {b : α} {c : α} {d : α} [MulZeroClass α] [Preorder α] [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} {a : α} {b : α} {c : α} {d : α} [MulZeroClass α] [Preorder α] [MulPosMono α] (h : a ≤ b * c) (hle : b ≤ d) (c0 : 0 ≤ c) : a ≤ d * c

theorem posMulMono_iff_covariant_pos {α : Type u_1} [MulZeroClass α] [PartialOrder α] : PosMulMono α ↔ CovariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x x_1 => x ≤ x_1

theorem mulPosMono_iff_covariant_pos {α : Type u_1} [MulZeroClass α] [PartialOrder α] : MulPosMono α ↔ CovariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x x_1 => x ≤ x_1

theorem posMulReflectLT_iff_contravariant_pos {α : Type u_1} [MulZeroClass α] [PartialOrder α] : PosMulReflectLT α ↔ ContravariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x x_1 => x < x_1

theorem mulPosReflectLT_iff_contravariant_pos {α : Type u_1} [MulZeroClass α] [PartialOrder α] : MulPosReflectLT α ↔ ContravariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x x_1 => x < x_1

instance PosMulStrictMono.toPosMulMono {α : Type u_1} [MulZeroClass α] [PartialOrder α] [PosMulStrictMono α] : PosMulMono α

instance MulPosStrictMono.toMulPosMono {α : Type u_1} [MulZeroClass α] [PartialOrder α] [MulPosStrictMono α] : MulPosMono α

instance PosMulMonoRev.toPosMulReflectLT {α : Type u_1} [MulZeroClass α] [PartialOrder α] [PosMulMonoRev α] : PosMulReflectLT α

instance MulPosMonoRev.toMulPosReflectLT {α : Type u_1} [MulZeroClass α] [PartialOrder α] [MulPosMonoRev α] : MulPosReflectLT α

theorem mul_left_cancel_iff_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [MulZeroClass α] [PartialOrder α] [PosMulMonoRev α] (a0 : 0 < a) : a * b = a * c ↔ b = c

theorem mul_right_cancel_iff_of_pos {α : Type u_1} {a : α} {b : α} {c : α} [MulZeroClass α] [PartialOrder α] [MulPosMonoRev α] (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 : α} [MulZeroClass α] [PartialOrder α] [PosMulStrictMono α] [MulPosStrictMono α] (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 : α} [MulZeroClass α] [PartialOrder α] [PosMulStrictMono α] [MulPosStrictMono α] (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 : α} [MulZeroClass α] [LinearOrder α] [PosMulMono α] [MulPosMono α] (hab : 0 < a * b) : 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

theorem neg_of_mul_pos_right {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [LinearOrder α] [PosMulMono α] [MulPosMono α] (h : 0 < a * b) (ha : a ≤ 0) : b < 0

theorem neg_of_mul_pos_left {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [LinearOrder α] [PosMulMono α] [MulPosMono α] (h : 0 < a * b) (ha : b ≤ 0) : a < 0

theorem neg_iff_neg_of_mul_pos {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [LinearOrder α] [PosMulMono α] [MulPosMono α] (hab : 0 < a * b) : a < 0 ↔ b < 0

theorem Left.neg_of_mul_neg_left {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [LinearOrder α] [PosMulMono α] (h : a * b < 0) (h1 : 0 ≤ a) : b < 0

theorem Right.neg_of_mul_neg_left {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [LinearOrder α] [MulPosMono α] (h : a * b < 0) (h1 : 0 ≤ a) : b < 0

theorem Left.neg_of_mul_neg_right {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [LinearOrder α] [PosMulMono α] (h : a * b < 0) (h1 : 0 ≤ b) : a < 0

theorem Right.neg_of_mul_neg_right {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [LinearOrder α] [MulPosMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] [PosMulMonoRev α] (a0 : 0 < a) : a ≤ a * b ↔ 1 ≤ b

@[simp]

theorem lt_mul_iff_one_lt_right {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) : a < a * b ↔ 1 < b

@[simp]

theorem mul_le_iff_le_one_right {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] [PosMulMonoRev α] (a0 : 0 < a) : a * b ≤ a ↔ b ≤ 1

@[simp]

theorem mul_lt_iff_lt_one_right {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] [PosMulReflectLT α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] [MulPosMonoRev α] (a0 : 0 < a) : a ≤ b * a ↔ 1 ≤ b

@[simp]

theorem lt_mul_iff_one_lt_left {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] [MulPosReflectLT α] (a0 : 0 < a) : a < b * a ↔ 1 < b

@[simp]

theorem mul_le_iff_le_one_left {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] [MulPosMonoRev α] (b0 : 0 < b) : a * b ≤ b ↔ a ≤ 1

@[simp]

theorem mul_lt_iff_lt_one_left {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] [MulPosReflectLT α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (hb : 0 ≤ b) (h : a ≤ 1) : a * b ≤ b

theorem le_mul_of_one_le_left {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (hb : 0 ≤ b) (h : 1 ≤ a) : b ≤ a * b

theorem mul_le_of_le_one_right {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (ha : 0 ≤ a) (h : b ≤ 1) : a * b ≤ a

theorem le_mul_of_one_le_right {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (ha : 0 ≤ a) (h : 1 ≤ b) : a ≤ a * b

theorem mul_lt_of_lt_one_left {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] (hb : 0 < b) (h : a < 1) : a * b < b

theorem lt_mul_of_one_lt_left {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] (hb : 0 < b) (h : 1 < a) : b < a * b

theorem mul_lt_of_lt_one_right {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] (ha : 0 < a) (h : b < 1) : a * b < a

theorem lt_mul_of_one_lt_right {α : Type u_1} {a : α} {b : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] [MulPosMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] [MulPosStrictMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] [MulPosMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] [MulPosStrictMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] [MulPosMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] [MulPosMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] [MulPosStrictMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] [MulPosStrictMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] [MulPosStrictMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] [MulPosMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] [MulPosStrictMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulStrictMono α] [MulPosMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosStrictMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [PosMulMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (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 : α} [MulOneClass α] [Zero α] [Preorder α] [MulPosMono α] (h : a ≤ b * c) (hb : b ≤ 1) (hc : 0 ≤ c) : a ≤ c

theorem exists_square_le' {α : Type u_1} {a : α} [MulOneClass α] [Zero α] [LinearOrder α] [PosMulStrictMono α] (a0 : 0 < a) : ∃ b, b * b ≤ a

theorem PosMulMono.toPosMulStrictMono {α : Type u_1} [CancelMonoidWithZero α] [PartialOrder α] [PosMulMono α] : PosMulStrictMono α

theorem posMulMono_iff_posMulStrictMono {α : Type u_1} [CancelMonoidWithZero α] [PartialOrder α] : PosMulMono α ↔ PosMulStrictMono α

theorem MulPosMono.toMulPosStrictMono {α : Type u_1} [CancelMonoidWithZero α] [PartialOrder α] [MulPosMono α] : MulPosStrictMono α

theorem mulPosMono_iff_mulPosStrictMono {α : Type u_1} [CancelMonoidWithZero α] [PartialOrder α] : MulPosMono α ↔ MulPosStrictMono α

theorem PosMulReflectLT.toPosMulMonoRev {α : Type u_1} [CancelMonoidWithZero α] [PartialOrder α] [PosMulReflectLT α] : PosMulMonoRev α

theorem posMulMonoRev_iff_posMulReflectLT {α : Type u_1} [CancelMonoidWithZero α] [PartialOrder α] : PosMulMonoRev α ↔ PosMulReflectLT α

theorem MulPosReflectLT.toMulPosMonoRev {α : Type u_1} [CancelMonoidWithZero α] [PartialOrder α] [MulPosReflectLT α] : MulPosMonoRev α

theorem mulPosMonoRev_iff_mulPosReflectLT {α : Type u_1} [CancelMonoidWithZero α] [PartialOrder α] : MulPosMonoRev α ↔ MulPosReflectLT α

theorem posMulStrictMono_iff_mulPosStrictMono {α : Type u_1} [Mul α] [IsSymmOp α α fun x x_1 => x * x_1] [Zero α] [Preorder α] : PosMulStrictMono α ↔ MulPosStrictMono α

theorem posMulReflectLT_iff_mulPosReflectLT {α : Type u_1} [Mul α] [IsSymmOp α α fun x x_1 => x * x_1] [Zero α] [Preorder α] : PosMulReflectLT α ↔ MulPosReflectLT α

theorem posMulMono_iff_mulPosMono {α : Type u_1} [Mul α] [IsSymmOp α α fun x x_1 => x * x_1] [Zero α] [Preorder α] : PosMulMono α ↔ MulPosMono α

theorem posMulMonoRev_iff_mulPosMonoRev {α : Type u_1} [Mul α] [IsSymmOp α α fun x x_1 => x * x_1] [Zero α] [Preorder α] : PosMulMonoRev α ↔ MulPosMonoRev α