Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

Left.mul_pos theorem

[PosMulStrictMono α] (ha : 0 < a) (hb : 0 < b) : 0 < a * b

Full source

/-- Assumes left covariance. -/
theorem Left.mul_pos [PosMulStrictMono α] (ha : 0 < a) (hb : 0 < b) : 0 < a * b := by
  simpa only [mul_zero] using mul_lt_mul_of_pos_left hb ha

Positivity of Product under Left Monotonicity: $a > 0 \land b > 0 \implies a \cdot b > 0$

Informal description

Let $\alpha$ be a preorder with a multiplication operation such that left multiplication by positive elements is strictly monotone. For any positive elements $a > 0$ and $b > 0$ in $\alpha$, their product satisfies $a \cdot b > 0$.

mul_neg_of_pos_of_neg theorem

[PosMulStrictMono α] (ha : 0 < a) (hb : b < 0) : a * b < 0

Full source

theorem mul_neg_of_pos_of_neg [PosMulStrictMono α] (ha : 0 < a) (hb : b < 0) : a * b < 0 := by
  simpa only [mul_zero] using mul_lt_mul_of_pos_left hb ha

Product of Positive and Negative Elements is Negative under Left Monotonicity

Informal description

Let $\alpha$ be a preorder with a multiplication operation such that left multiplication by positive elements is strictly monotone. For any positive element $a > 0$ and any negative element $b < 0$ in $\alpha$, their product satisfies $a \cdot b < 0$.

mul_pos_iff_of_pos_left theorem

[PosMulStrictMono α] [PosMulReflectLT α] (h : 0 < a) : 0 < a * b ↔ 0 < b

Full source

@[simp]
theorem mul_pos_iff_of_pos_left [PosMulStrictMono α] [PosMulReflectLT α] (h : 0 < a) :
    0 < a * b ↔ 0 < b := by simpa using mul_lt_mul_left (b := 0) h

Positivity of Product under Left Multiplication by Positive Elements

Informal description

Let $\alpha$ be a preorder with a multiplication operation such that left multiplication by positive elements is strictly monotone and reflects the strict order. For any positive element $a > 0$ and any element $b \in \alpha$, the product $a \cdot b$ is positive if and only if $b$ is positive, i.e., \[ a \cdot b > 0 \leftrightarrow b > 0. \]

Right.mul_pos theorem

[MulPosStrictMono α] (ha : 0 < a) (hb : 0 < b) : 0 < a * b

Full source

/-- Assumes right covariance. -/
theorem Right.mul_pos [MulPosStrictMono α] (ha : 0 < a) (hb : 0 < b) : 0 < a * b := by
  simpa only [zero_mul] using mul_lt_mul_of_pos_right ha hb

Product of Positive Elements is Positive under Right Monotonicity

Informal description

Let $\alpha$ be a preorder with a multiplication operation where right multiplication by positive elements is strictly monotone. For any positive elements $a > 0$ and $b > 0$ in $\alpha$, their product satisfies $a \cdot b > 0$.

mul_neg_of_neg_of_pos theorem

[MulPosStrictMono α] (ha : a < 0) (hb : 0 < b) : a * b < 0

Full source

theorem mul_neg_of_neg_of_pos [MulPosStrictMono α] (ha : a < 0) (hb : 0 < b) : a * b < 0 := by
  simpa only [zero_mul] using mul_lt_mul_of_pos_right ha hb

Product of Negative and Positive is Negative: $a < 0 \land b > 0 \implies a \cdot b < 0$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where right multiplication by positive elements is strictly monotone (i.e., `MulPosStrictMono α` holds). Then for any element $a < 0$ and any positive element $b > 0$, their product satisfies $a \cdot b < 0$.

mul_pos_iff_of_pos_right theorem

[MulPosStrictMono α] [MulPosReflectLT α] (h : 0 < b) : 0 < a * b ↔ 0 < a

Full source

@[simp]
theorem mul_pos_iff_of_pos_right [MulPosStrictMono α] [MulPosReflectLT α] (h : 0 < b) :
    0 < a * b ↔ 0 < a := by simpa using mul_lt_mul_right (b := 0) h

Positivity of Product under Right Multiplication by Positive Elements: $b > 0 \implies (a \cdot b > 0 \leftrightarrow a > 0)$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where right multiplication by positive elements is strictly monotone and reflects the strict order. For any positive element $b > 0$ in $\alpha$, the product $a \cdot b$ is positive if and only if $a$ is positive, i.e., \[ 0 < a \cdot b \leftrightarrow 0 < a. \]

Left.mul_nonneg theorem

[PosMulMono α] (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b

Full source

/-- Assumes left covariance. -/
theorem Left.mul_nonneg [PosMulMono α] (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b := by
  simpa only [mul_zero] using mul_le_mul_of_nonneg_left hb ha

Nonnegativity of Product under Left Monotonicity: $a, b \geq 0 \implies a \cdot b \geq 0$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where left multiplication by nonnegative elements is monotone (i.e., `PosMulMono α` holds). Then for any nonnegative elements $a, b \in \alpha$ (i.e., $a \geq 0$ and $b \geq 0$), their product $a \cdot b$ is also nonnegative, i.e., $a \cdot b \geq 0$.

mul_nonpos_of_nonneg_of_nonpos theorem

[PosMulMono α] (ha : 0 ≤ a) (hb : b ≤ 0) : a * b ≤ 0

Full source

theorem mul_nonpos_of_nonneg_of_nonpos [PosMulMono α] (ha : 0 ≤ a) (hb : b ≤ 0) : a * b ≤ 0 := by
  simpa only [mul_zero] using mul_le_mul_of_nonneg_left hb ha

Nonpositivity of Product of Nonnegative and Nonpositive Elements under Left Monotonicity

Informal description

Let $\alpha$ be a preorder with a multiplication operation where left multiplication by nonnegative elements is monotone (i.e., `PosMulMono α` holds). Then for any nonnegative element $a \in \alpha$ (i.e., $a \geq 0$) and any nonpositive element $b \in \alpha$ (i.e., $b \leq 0$), their product $a \cdot b$ is nonpositive, i.e., $a \cdot b \leq 0$.

Right.mul_nonneg theorem

[MulPosMono α] (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b

Full source

/-- Assumes right covariance. -/
theorem Right.mul_nonneg [MulPosMono α] (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b := by
  simpa only [zero_mul] using mul_le_mul_of_nonneg_right ha hb

Nonnegativity of Product under Right Monotonicity: $a, b \geq 0 \implies a \cdot b \geq 0$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where right multiplication by nonnegative elements is monotone (i.e., `MulPosMono α` holds). Then for any nonnegative elements $a, b \in \alpha$ (i.e., $a \geq 0$ and $b \geq 0$), their product $a \cdot b$ is also nonnegative, i.e., $a \cdot b \geq 0$.

mul_nonpos_of_nonpos_of_nonneg theorem

[MulPosMono α] (ha : a ≤ 0) (hb : 0 ≤ b) : a * b ≤ 0

Full source

theorem mul_nonpos_of_nonpos_of_nonneg [MulPosMono α] (ha : a ≤ 0) (hb : 0 ≤ b) : a * b ≤ 0 := by
  simpa only [zero_mul] using mul_le_mul_of_nonneg_right ha hb

Nonpositivity of Product of Nonpositive and Nonnegative Elements under Right Monotonicity

Informal description

Let $\alpha$ be a preorder with a multiplication operation where right multiplication by nonnegative elements is monotone (i.e., `MulPosMono α` holds). Then for any nonpositive element $a \in \alpha$ (i.e., $a \leq 0$) and any nonnegative element $b \in \alpha$ (i.e., $b \geq 0$), their product $a \cdot b$ is nonpositive, i.e., $a \cdot b \leq 0$.

pos_of_mul_pos_right theorem

[PosMulReflectLT α] (h : 0 < a * b) (ha : 0 ≤ a) : 0 < b

Full source

theorem pos_of_mul_pos_right [PosMulReflectLT α] (h : 0 < a * b) (ha : 0 ≤ a) : 0 < b :=
  lt_of_mul_lt_mul_left ((mul_zero a).symm ▸ h : a * 0 < a * b) ha

Positivity of Right Factor from Positive Product via Left Multiplication

Informal description

Let $\alpha$ be a preorder with a multiplication operation where left multiplication by nonnegative elements reflects the strict order (i.e., `PosMulReflectLT α` holds). If $0 < a \cdot b$ and $0 \leq a$, then $0 < b$.

pos_of_mul_pos_left theorem

[MulPosReflectLT α] (h : 0 < a * b) (hb : 0 ≤ b) : 0 < a

Full source

theorem pos_of_mul_pos_left [MulPosReflectLT α] (h : 0 < a * b) (hb : 0 ≤ b) : 0 < a :=
  lt_of_mul_lt_mul_right ((zero_mul b).symm ▸ h : 0 * b < a * b) hb

Positivity from Left Factor in Product: $0 < a \cdot b \land 0 \leq b \implies 0 < a$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where right multiplication by nonnegative elements reflects the strict order (i.e., `MulPosReflectLT α` holds). If $0 < a \cdot b$ and $0 \leq b$, then $0 < a$.

pos_iff_pos_of_mul_pos theorem

[PosMulReflectLT α] [MulPosReflectLT α] (hab : 0 < a * b) : 0 < a ↔ 0 < b

Full source

theorem pos_iff_pos_of_mul_pos [PosMulReflectLT α] [MulPosReflectLT α] (hab : 0 < a * b) :
    0 < a ↔ 0 < b :=
  ⟨pos_of_mul_pos_right hab ∘ le_of_lt, pos_of_mul_pos_left hab ∘ le_of_lt⟩

Positivity Equivalence in Product: $0 < a \cdot b \implies (0 < a \leftrightarrow 0 < b)$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where left multiplication by nonnegative elements reflects the strict order (`PosMulReflectLT α`) and right multiplication by nonnegative elements reflects the strict order (`MulPosReflectLT α`). For any elements $a, b \in \alpha$ with $0 < a \cdot b$, we have $0 < a$ if and only if $0 < b$.

Left.mul_lt_mul_of_nonneg theorem

[PosMulStrictMono α] [MulPosMono α] (h₁ : a < b) (h₂ : c < d) (a0 : 0 ≤ a) (c0 : 0 ≤ c) : a * c < b * d

Full source

/-- Assumes left strict covariance. -/
theorem Left.mul_lt_mul_of_nonneg [PosMulStrictMono α] [MulPosMono α]
    (h₁ : a < b) (h₂ : c < d) (a0 : 0 ≤ a) (c0 : 0 ≤ c) : a * c < b * d :=
  mul_lt_mul_of_le_of_lt_of_nonneg_of_pos h₁.le h₂ c0 (a0.trans_lt h₁)

Strict Inequality Preservation Under Nonnegative Multiplication: Left Variant

Informal description

Let $\alpha$ be a preorder with a multiplication operation where left multiplication by positive elements is strictly monotone (`PosMulStrictMono α`) and right multiplication by nonnegative elements is monotone (`MulPosMono α`). For any elements $a, b, c, d \in \alpha$ with $a < b$ and $c < d$, and any nonnegative elements $a \geq 0$ and $c \geq 0$, we have $a \cdot c < b \cdot d$.

Right.mul_lt_mul_of_nonneg theorem

[PosMulMono α] [MulPosStrictMono α] (h₁ : a < b) (h₂ : c < d) (a0 : 0 ≤ a) (c0 : 0 ≤ c) : a * c < b * d

Full source

/-- Assumes right strict covariance. -/
theorem Right.mul_lt_mul_of_nonneg [PosMulMono α] [MulPosStrictMono α]
    (h₁ : a < b) (h₂ : c < d) (a0 : 0 ≤ a) (c0 : 0 ≤ c) : a * c < b * d :=
  mul_lt_mul_of_lt_of_le_of_nonneg_of_pos h₁ h₂.le a0 (c0.trans_lt h₂)

Strict Inequality Preservation Under Nonnegative Multiplication: Right Variant

Informal description

Let $\alpha$ be a preorder with a multiplication operation where left multiplication by nonnegative elements is monotone (`PosMulMono α`) and right multiplication by nonnegative elements is strictly monotone (`MulPosStrictMono α`). For any elements $a, b, c, d \in \alpha$ with $a < b$ and $c < d$, and any nonnegative elements $a \geq 0$ and $c \geq 0$, we have $a \cdot c < b \cdot d$.

mul_self_le_mul_self theorem

[PosMulMono α] [MulPosMono α] (ha : 0 ≤ a) (hab : a ≤ b) : a * a ≤ b * b

Full source

theorem mul_self_le_mul_self [PosMulMono α] [MulPosMono α] (ha : 0 ≤ a) (hab : a ≤ b) :
    a * a ≤ b * b :=
  mul_le_mul hab hab ha <| ha.trans hab

Monotonicity of Squaring for Nonnegative Elements: $0 \leq a \leq b \implies a^2 \leq b^2$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where left and right multiplication by nonnegative elements are both monotone (i.e., $\alpha$ satisfies `PosMulMono` and `MulPosMono`). For any elements $a, b \in \alpha$ with $0 \leq a$ and $a \leq b$, we have $a^2 \leq b^2$.

posMulMono_iff_covariant_pos theorem

: PosMulMono α ↔ CovariantClass α>0 α (fun x y => x * y) (· ≤ ·)

Full source

theorem posMulMono_iff_covariant_pos :
    PosMulMonoPosMulMono α ↔ CovariantClass α>0 α (fun x y => x * y) (· ≤ ·) :=
  ⟨@PosMulMono.to_covariantClass_pos_mul_le _ _ _ _, fun h =>
    { elim a b c h := by
        obtain ha | ha := a.prop.eq_or_lt
        · simp [← ha]
        · exact @CovariantClass.elim α>0 α (fun x y => x * y) (· ≤ ·) _ ⟨_, ha⟩ _ _ h }⟩

Equivalence of Monotonicity and Covariant Left Multiplication by Positive Elements

Informal description

For a preordered type $\alpha$, the property that left multiplication by nonnegative elements is monotone is equivalent to the property that left multiplication by positive elements is covariant with respect to the order. That is, for all $a_1, a_2 \in \alpha$ and $b > 0$, we have $a_1 \leq a_2$ implies $b \cdot a_1 \leq b \cdot a_2$ if and only if $\alpha$ satisfies the `CovariantClass` condition for positive elements under left multiplication.

mulPosMono_iff_covariant_pos theorem

: MulPosMono α ↔ CovariantClass α>0 α (fun x y => y * x) (· ≤ ·)

Full source

theorem mulPosMono_iff_covariant_pos :
    MulPosMonoMulPosMono α ↔ CovariantClass α>0 α (fun x y => y * x) (· ≤ ·) :=
  ⟨@MulPosMono.to_covariantClass_pos_mul_le _ _ _ _, fun h =>
    { elim a b c h := by
        obtain ha | ha := a.prop.eq_or_lt
        · simp [← ha]
        · exact @CovariantClass.elim α>0 α (fun x y => y * x) (· ≤ ·) _ ⟨_, ha⟩ _ _ h }⟩

Equivalence of Monotonicity and Covariant Right Multiplication by Positive Elements

Informal description

For a preordered type $\alpha$, the property that right multiplication by nonnegative elements is monotone is equivalent to the property that right multiplication by positive elements is covariant with respect to the order. That is, for all $a_1, a_2 \in \alpha$ and $b > 0$, we have $a_1 \leq a_2$ implies $a_1 \cdot b \leq a_2 \cdot b$ if and only if $\alpha$ satisfies the `CovariantClass` condition for positive elements under right multiplication.

posMulReflectLT_iff_contravariant_pos theorem

: PosMulReflectLT α ↔ ContravariantClass α>0 α (fun x y => x * y) (· < ·)

Full source

theorem posMulReflectLT_iff_contravariant_pos :
    PosMulReflectLTPosMulReflectLT α ↔ ContravariantClass α>0 α (fun x y => x * y) (· < ·) :=
  ⟨@PosMulReflectLT.to_contravariantClass_pos_mul_lt _ _ _ _, fun h =>
    { elim a b c h := by
        obtain ha | ha := a.prop.eq_or_lt
        · simp [← ha] at h
        · exact @ContravariantClass.elim α>0 α (fun x y => x * y) (· < ·) _ ⟨_, ha⟩ _ _ h }⟩

Equivalence of Strict Order Reflection and Contravariant Left Multiplication by Positive Elements

Informal description

For a preorder $\alpha$, the property that left multiplication by nonnegative elements reflects the strict order is equivalent to the property that left multiplication by positive elements is contravariant with respect to the strict order. That is, for all $a_1, a_2 \in \alpha$ and $b > 0$, we have $b \cdot a_1 < b \cdot a_2$ if and only if $a_1 < a_2$.

mulPosReflectLT_iff_contravariant_pos theorem

: MulPosReflectLT α ↔ ContravariantClass α>0 α (fun x y => y * x) (· < ·)

Full source

theorem mulPosReflectLT_iff_contravariant_pos :
    MulPosReflectLTMulPosReflectLT α ↔ ContravariantClass α>0 α (fun x y => y * x) (· < ·) :=
  ⟨@MulPosReflectLT.to_contravariantClass_pos_mul_lt _ _ _ _, fun h =>
    { elim a b c h := by
        obtain ha | ha := a.prop.eq_or_lt
        · simp [← ha] at h
        · exact @ContravariantClass.elim α>0 α (fun x y => y * x) (· < ·) _ ⟨_, ha⟩ _ _ h }⟩

Equivalence of Strict Order Reflection and Contravariant Right Multiplication by Positive Elements

Informal description

For a preorder $\alpha$, the property that right multiplication by nonnegative elements reflects the strict order is equivalent to the property that right multiplication by positive elements is contravariant with respect to the strict order. That is, for all $a_1, a_2 \in \alpha$ and $b > 0$, we have $a_1 * b < a_2 * b$ if and only if $a_1 < a_2$.

PosMulStrictMono.toPosMulMono instance

[PosMulStrictMono α] : PosMulMono α

Full source

instance (priority := 100) PosMulStrictMono.toPosMulMono [PosMulStrictMono α] : PosMulMono α :=
  posMulMono_iff_covariant_pos.2 (covariantClass_le_of_lt _ _ _)

Strict Monotonicity Implies Monotonicity for Left Multiplication by Nonnegative Elements

Informal description

Every type $\alpha$ with strictly monotone left multiplication by positive elements also has monotone left multiplication by nonnegative elements. That is, if for all $b > 0$ and $a_1 < a_2$ we have $b \cdot a_1 < b \cdot a_2$, then for all $b \geq 0$ and $a_1 \leq a_2$ we have $b \cdot a_1 \leq b \cdot a_2$.

MulPosStrictMono.toMulPosMono instance

[MulPosStrictMono α] : MulPosMono α

Full source

instance (priority := 100) MulPosStrictMono.toMulPosMono [MulPosStrictMono α] : MulPosMono α :=
  mulPosMono_iff_covariant_pos.2 (covariantClass_le_of_lt _ _ _)

Strict Monotonicity Implies Monotonicity for Right Multiplication by Nonnegative Elements

Informal description

Every preorder $\alpha$ with strictly monotone right multiplication by positive elements also has monotone right multiplication by nonnegative elements. That is, if for all $b > 0$ and $a_1 < a_2$ we have $a_1 \cdot b < a_2 \cdot b$, then for all $b \geq 0$ and $a_1 \leq a_2$ we have $a_1 \cdot b \leq a_2 \cdot b$.

PosMulReflectLE.toPosMulReflectLT instance

[PosMulReflectLE α] : PosMulReflectLT α

Full source

instance (priority := 100) PosMulReflectLE.toPosMulReflectLT [PosMulReflectLE α] :
    PosMulReflectLT α :=
  posMulReflectLT_iff_contravariant_pos.2
    ⟨fun a b c h =>
      (le_of_mul_le_mul_of_pos_left h.le a.2).lt_of_ne <| by
        rintro rfl
        simp at h⟩

Reflection of Strict Order from Non-Strict Order under Left Multiplication by Nonnegative Elements

Informal description

For any preorder $\alpha$ where left multiplication by positive elements reflects the non-strict order (i.e., $b \cdot a_1 \leq b \cdot a_2$ implies $a_1 \leq a_2$ for $b > 0$), left multiplication by nonnegative elements also reflects the strict order (i.e., $b \cdot a_1 < b \cdot a_2$ implies $a_1 < a_2$ for $b \geq 0$).

MulPosReflectLE.toMulPosReflectLT instance

[MulPosReflectLE α] : MulPosReflectLT α

Full source

instance (priority := 100) MulPosReflectLE.toMulPosReflectLT [MulPosReflectLE α] :
    MulPosReflectLT α :=
  mulPosReflectLT_iff_contravariant_pos.2
    ⟨fun a b c h =>
      (le_of_mul_le_mul_of_pos_right h.le a.2).lt_of_ne <| by
        rintro rfl
        simp at h⟩

Reflection of Strict Order from Non-Strict Order under Right Multiplication by Nonnegative Elements

Informal description

For any preorder $\alpha$ where right multiplication by positive elements reflects the non-strict order (i.e., $a_1 * b \leq a_2 * b$ implies $a_1 \leq a_2$ for $b > 0$), right multiplication by nonnegative elements also reflects the strict order (i.e., $a_1 * b < a_2 * b$ implies $a_1 < a_2$ for $b \geq 0$).

mul_left_cancel_iff_of_pos theorem

[PosMulReflectLE α] (a0 : 0 < a) : a * b = a * c ↔ b = c

Full source

theorem mul_left_cancel_iff_of_pos [PosMulReflectLE α] (a0 : 0 < a) : a * b = a * c ↔ b = c :=
  ⟨fun h => (le_of_mul_le_mul_of_pos_left h.le a0).antisymm <|
    le_of_mul_le_mul_of_pos_left h.ge a0, congr_arg _⟩

Left cancellation property for multiplication by positive elements: $a \cdot b = a \cdot c \leftrightarrow b = c$ when $a > 0$

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder, such that left multiplication by positive elements reflects the non-strict order (i.e., $b \cdot a_1 \leq b \cdot a_2$ implies $a_1 \leq a_2$ for $b > 0$). Then for any positive element $a > 0$ in $\alpha$, the equation $a \cdot b = a \cdot c$ holds if and only if $b = c$.

mul_right_cancel_iff_of_pos theorem

[MulPosReflectLE α] (b0 : 0 < b) : a * b = c * b ↔ a = c

Full source

theorem mul_right_cancel_iff_of_pos [MulPosReflectLE α] (b0 : 0 < b) : a * b = c * b ↔ a = c :=
  ⟨fun h => (le_of_mul_le_mul_of_pos_right h.le b0).antisymm <|
    le_of_mul_le_mul_of_pos_right h.ge b0, congr_arg (· * b)⟩

Right cancellation property for multiplication by positive elements: $a * b = c * b \leftrightarrow a = c$ when $b > 0$

Informal description

Let $\alpha$ be a type with a multiplication operation and a preorder, such that right multiplication by positive elements reflects the non-strict order (i.e., $a_1 * b \leq a_2 * b$ implies $a_1 \leq a_2$ for $b > 0$). Then for any positive element $b > 0$ in $\alpha$, the equation $a * b = c * b$ holds if and only if $a = c$.

mul_eq_mul_iff_eq_and_eq_of_pos theorem

 [PosMulStrictMono α] [MulPosStrictMono α] (hab : a ≤ b) (hcd : c ≤ d) (a0 : 0 < a) (d0 : 0 < d) :
  a * c = b * d ↔ a = b ∧ c = d

Full source

theorem mul_eq_mul_iff_eq_and_eq_of_pos [PosMulStrictMono α] [MulPosStrictMono α]
    (hab : a ≤ b) (hcd : c ≤ d) (a0 : 0 < a) (d0 : 0 < d) :
    a * c = b * d ↔ a = b ∧ c = d := by
  refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
  simp only [eq_iff_le_not_lt, hab, hcd, true_and]
  refine ⟨fun hab ↦ h.not_lt ?_, fun hcd ↦ h.not_lt ?_⟩
  · exact (mul_le_mul_of_nonneg_left hcd a0.le).trans_lt (mul_lt_mul_of_pos_right hab d0)
  · exact (mul_lt_mul_of_pos_left hcd a0).trans_le (mul_le_mul_of_nonneg_right hab d0.le)

Equality of Products under Strict Monotonicity: $a \cdot c = b \cdot d \leftrightarrow a = b \land c = d$ for $a \leq b$, $c \leq d$, $a > 0$, $d > 0$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where left and right multiplication by positive elements are strictly monotone (i.e., `PosMulStrictMono α` and `MulPosStrictMono α` hold). For any elements $a, b, c, d \in \alpha$ such that $a \leq b$, $c \leq d$, $a > 0$, and $d > 0$, the equality $a \cdot c = b \cdot d$ holds if and only if $a = b$ and $c = d$.

mul_eq_mul_iff_eq_and_eq_of_pos' theorem

 [PosMulStrictMono α] [MulPosStrictMono α] (hab : a ≤ b) (hcd : c ≤ d) (b0 : 0 < b) (c0 : 0 < c) :
  a * c = b * d ↔ a = b ∧ c = d

Full source

theorem mul_eq_mul_iff_eq_and_eq_of_pos' [PosMulStrictMono α] [MulPosStrictMono α]
    (hab : a ≤ b) (hcd : c ≤ d) (b0 : 0 < b) (c0 : 0 < c) :
    a * c = b * d ↔ a = b ∧ c = d := by
  refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
  simp only [eq_iff_le_not_lt, hab, hcd, true_and]
  refine ⟨fun hab ↦ h.not_lt ?_, fun hcd ↦ h.not_lt ?_⟩
  · exact (mul_lt_mul_of_pos_right hab c0).trans_le (mul_le_mul_of_nonneg_left hcd b0.le)
  · exact (mul_le_mul_of_nonneg_right hab c0.le).trans_lt (mul_lt_mul_of_pos_left hcd b0)

Equality of Products under Strict Monotonicity: $a \cdot c = b \cdot d \leftrightarrow a = b \land c = d$ for $a \leq b$, $c \leq d$, $b > 0$, $c > 0$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where left and right multiplication by positive elements are strictly monotone (i.e., `PosMulStrictMono α` and `MulPosStrictMono α` hold). For any elements $a, b, c, d \in \alpha$ such that $a \leq b$, $c \leq d$, $b > 0$, and $c > 0$, the equality $a \cdot c = b \cdot d$ holds if and only if $a = b$ and $c = d$.

pos_and_pos_or_neg_and_neg_of_mul_pos theorem

[PosMulMono α] [MulPosMono α] (hab : 0 < a * b) : 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Full source

theorem pos_and_pos_or_neg_and_neg_of_mul_pos [PosMulMono α] [MulPosMono α] (hab : 0 < a * b) :
    0 < a ∧ 0 < b0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 := by
  rcases lt_trichotomy a 0 with (ha | rfl | ha)
  · refine Or.inr ⟨ha, lt_imp_lt_of_le_imp_le (fun hb => ?_) hab⟩
    exact mul_nonpos_of_nonpos_of_nonneg ha.le hb
  · rw [zero_mul] at hab
    exact hab.false.elim
  · refine Or.inl ⟨ha, lt_imp_lt_of_le_imp_le (fun hb => ?_) hab⟩
    exact mul_nonpos_of_nonneg_of_nonpos ha.le hb

Product Positivity Implies Both Positive or Both Negative

Informal description

Let $\alpha$ be a preorder with a multiplication operation where both left and right multiplication by nonnegative elements are monotone (i.e., `PosMulMono α` and `MulPosMono α` hold). For any elements $a, b \in \alpha$ such that their product is positive ($a \cdot b > 0$), either both $a$ and $b$ are positive ($a > 0$ and $b > 0$) or both are negative ($a < 0$ and $b < 0$).

neg_of_mul_pos_right theorem

[PosMulMono α] [MulPosMono α] (h : 0 < a * b) (ha : a ≤ 0) : b < 0

Full source

theorem neg_of_mul_pos_right [PosMulMono α] [MulPosMono α] (h : 0 < a * b) (ha : a ≤ 0) : b < 0 :=
  ((pos_and_pos_or_neg_and_neg_of_mul_pos h).resolve_left fun h => h.1.not_le ha).2

Negativity of Second Factor Given Nonpositive First Factor and Positive Product

Informal description

Let $\alpha$ be a preorder with a multiplication operation where both left and right multiplication by nonnegative elements are monotone (i.e., `PosMulMono α` and `MulPosMono α` hold). For any elements $a, b \in \alpha$ such that their product is positive ($a \cdot b > 0$) and $a \leq 0$, it follows that $b < 0$.

neg_of_mul_pos_left theorem

[PosMulMono α] [MulPosMono α] (h : 0 < a * b) (ha : b ≤ 0) : a < 0

Full source

theorem neg_of_mul_pos_left [PosMulMono α] [MulPosMono α] (h : 0 < a * b) (ha : b ≤ 0) : a < 0 :=
  ((pos_and_pos_or_neg_and_neg_of_mul_pos h).resolve_left fun h => h.2.not_le ha).1

Negativity of Left Factor in Positive Product when Right Factor is Nonpositive

Informal description

Let $\alpha$ be a preorder with a multiplication operation where both left and right multiplication by nonnegative elements are monotone (i.e., `PosMulMono α` and `MulPosMono α` hold). For any elements $a, b \in \alpha$ such that their product is positive ($a \cdot b > 0$) and $b$ is nonpositive ($b \leq 0$), then $a$ must be negative ($a < 0$).

neg_iff_neg_of_mul_pos theorem

[PosMulMono α] [MulPosMono α] (hab : 0 < a * b) : a < 0 ↔ b < 0

Full source

theorem neg_iff_neg_of_mul_pos [PosMulMono α] [MulPosMono α] (hab : 0 < a * b) : a < 0 ↔ b < 0 :=
  ⟨neg_of_mul_pos_right hab ∘ le_of_lt, neg_of_mul_pos_left hab ∘ le_of_lt⟩

Negativity Equivalence in Positive Product under Monotonicity

Informal description

Let $\alpha$ be a preorder with a multiplication operation where both left and right multiplication by nonnegative elements are monotone (i.e., `PosMulMono α` and `MulPosMono α` hold). For any elements $a, b \in \alpha$ such that their product is positive ($a \cdot b > 0$), we have $a < 0$ if and only if $b < 0$.

Left.neg_of_mul_neg_right theorem

[PosMulMono α] (h : a * b < 0) (a0 : 0 ≤ a) : b < 0

Full source

theorem Left.neg_of_mul_neg_right [PosMulMono α] (h : a * b < 0) (a0 : 0 ≤ a) : b < 0 :=
  lt_of_not_ge fun b0 : b ≥ 0 => (Left.mul_nonneg a0 b0).not_lt h

Negativity of Right Factor in Negative Product under Left Monotonicity

Informal description

Let $\alpha$ be a preorder with a multiplication operation where left multiplication by nonnegative elements is monotone (i.e., `PosMulMono α` holds). If the product $a \cdot b$ is negative ($a \cdot b < 0$) and $a$ is nonnegative ($a \geq 0$), then $b$ must be negative ($b < 0$).

Right.neg_of_mul_neg_right theorem

[MulPosMono α] (h : a * b < 0) (a0 : 0 ≤ a) : b < 0

Full source

theorem Right.neg_of_mul_neg_right [MulPosMono α] (h : a * b < 0) (a0 : 0 ≤ a) : b < 0 :=
  lt_of_not_ge fun b0 : b ≥ 0 => (Right.mul_nonneg a0 b0).not_lt h

Negativity of Right Factor in Negative Product under Right Monotonicity

Informal description

Let $\alpha$ be a preorder with a multiplication operation where right multiplication by nonnegative elements is monotone (i.e., `MulPosMono α` holds). If the product $a \cdot b$ is negative ($a \cdot b < 0$) and $a$ is nonnegative ($a \geq 0$), then $b$ must be negative ($b < 0$).

Left.neg_of_mul_neg_left theorem

[PosMulMono α] (h : a * b < 0) (b0 : 0 ≤ b) : a < 0

Full source

theorem Left.neg_of_mul_neg_left [PosMulMono α] (h : a * b < 0) (b0 : 0 ≤ b) : a < 0 :=
  lt_of_not_ge fun a0 : a ≥ 0 => (Left.mul_nonneg a0 b0).not_lt h

Negativity of Left Factor from Negative Product under Left Monotonicity: $b \geq 0 \land a \cdot b < 0 \implies a < 0$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where left multiplication by nonnegative elements is monotone (i.e., `PosMulMono α` holds). For any elements $a, b \in \alpha$ such that $b \geq 0$ and $a \cdot b < 0$, it follows that $a < 0$.

Right.neg_of_mul_neg_left theorem

[MulPosMono α] (h : a * b < 0) (b0 : 0 ≤ b) : a < 0

Full source

theorem Right.neg_of_mul_neg_left [MulPosMono α] (h : a * b < 0) (b0 : 0 ≤ b) : a < 0 :=
  lt_of_not_ge fun a0 : a ≥ 0 => (Right.mul_nonneg a0 b0).not_lt h

Negativity of Left Factor from Negative Product under Right Monotonicity: $b \geq 0 \land a \cdot b < 0 \implies a < 0$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where right multiplication by nonnegative elements is monotone (i.e., `MulPosMono α` holds). For any elements $a, b \in \alpha$ such that $b \geq 0$ and $a \cdot b < 0$, it follows that $a < 0$.

one_lt_of_lt_mul_left₀ theorem

[PosMulReflectLT α] (ha : 0 ≤ a) (h : a < a * b) : 1 < b

Full source

lemma one_lt_of_lt_mul_left₀ [PosMulReflectLT α] (ha : 0 ≤ a) (h : a < a * b) : 1 < b :=
  lt_of_mul_lt_mul_left (by simpa) ha

Strict inequality from left multiplication by nonnegative elements: $a \geq 0 \land a < a \cdot b \implies 1 < b$

Informal description

Let $\alpha$ be a preorder with a multiplication operation and a zero element, such that left multiplication by nonnegative elements reflects the strict order (i.e., $\alpha$ satisfies `PosMulReflectLT`). For any nonnegative element $a \geq 0$ in $\alpha$, if $a < a \cdot b$, then $1 < b$.

one_lt_of_lt_mul_right₀ theorem

[MulPosReflectLT α] (hb : 0 ≤ b) (h : b < a * b) : 1 < a

Full source

lemma one_lt_of_lt_mul_right₀ [MulPosReflectLT α] (hb : 0 ≤ b) (h : b < a * b) : 1 < a :=
  lt_of_mul_lt_mul_right (by simpa) hb

Strict inequality from right multiplication by nonnegative elements: $b \geq 0 \land b < a \cdot b \implies 1 < a$

Informal description

Let $\alpha$ be a preorder with a multiplication operation and a zero element, such that right multiplication by nonnegative elements reflects the strict order (i.e., $\alpha$ satisfies `MulPosReflectLT`). For any nonnegative element $b \geq 0$ in $\alpha$, if $b < a \cdot b$, then $1 < a$.

one_le_of_le_mul_left₀ theorem

[PosMulReflectLE α] (ha : 0 < a) (h : a ≤ a * b) : 1 ≤ b

Full source

lemma one_le_of_le_mul_left₀ [PosMulReflectLE α] (ha : 0 < a) (h : a ≤ a * b) : 1 ≤ b :=
  le_of_mul_le_mul_left (by simpa) ha

Inequality from left multiplication by positive elements implies $1 \leq b$

Informal description

Let $\alpha$ be a preorder with a multiplication operation and a zero element, such that left multiplication by positive elements reflects the non-strict order (i.e., $\alpha$ satisfies `PosMulReflectLE`). For any positive element $a > 0$ in $\alpha$, if $a \leq a \cdot b$, then $1 \leq b$.

one_le_of_le_mul_right₀ theorem

[MulPosReflectLE α] (hb : 0 < b) (h : b ≤ a * b) : 1 ≤ a

Full source

lemma one_le_of_le_mul_right₀ [MulPosReflectLE α] (hb : 0 < b) (h : b ≤ a * b) : 1 ≤ a :=
  le_of_mul_le_mul_right (by simpa) hb

Non-strict order reflection under right multiplication by positive elements implies $1 \leq a$ when $b \leq a \cdot b$ for $b > 0$

Informal description

Let $\alpha$ be a preorder with a multiplication operation and a zero element, such that right multiplication by positive elements reflects the non-strict order (i.e., $\alpha$ satisfies `MulPosReflectLE`). For any positive element $b > 0$ in $\alpha$, if $b \leq a \cdot b$, then $1 \leq a$.

le_mul_iff_one_le_right theorem

[PosMulMono α] [PosMulReflectLE α] (a0 : 0 < a) : a ≤ a * b ↔ 1 ≤ b

Full source

@[simp]
lemma le_mul_iff_one_le_right [PosMulMono α] [PosMulReflectLE α] (a0 : 0 < a) : a ≤ a * b ↔ 1 ≤ b :=
  Iff.trans (by rw [mul_one]) (mul_le_mul_left a0)

Inequality Equivalence Under Left Multiplication by Positive Elements: $a > 0 \implies (a \leq a \cdot b \leftrightarrow 1 \leq b)$

Informal description

Let $\alpha$ be a preorder with a multiplication operation and a zero element, such that left multiplication by nonnegative elements is monotone (`PosMulMono α`) and left multiplication by positive elements reflects the non-strict order (`PosMulReflectLE α`). For any positive element $a > 0$ in $\alpha$, we have the equivalence: \[ a \leq a \cdot b \quad \text{if and only if} \quad 1 \leq b. \]

lt_mul_iff_one_lt_right theorem

[PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) : a < a * b ↔ 1 < b

Full source

@[simp]
theorem lt_mul_iff_one_lt_right [PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) :
    a < a * b ↔ 1 < b :=
  Iff.trans (by rw [mul_one]) (mul_lt_mul_left a0)

Strict Inequality Under Left Multiplication by Positive Elements: $a > 0 \implies (a < a \cdot b \leftrightarrow 1 < b)$

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If left multiplication by positive elements is strictly monotone (`PosMulStrictMono α`) and left multiplication by nonnegative elements reflects the strict order (`PosMulReflectLT α`), then for any positive element $a > 0$ and any element $b \in \alpha$, we have the equivalence: \[ a < a \cdot b \quad \text{if and only if} \quad 1 < b. \]

mul_le_iff_le_one_right theorem

[PosMulMono α] [PosMulReflectLE α] (a0 : 0 < a) : a * b ≤ a ↔ b ≤ 1

Full source

@[simp]
lemma mul_le_iff_le_one_right [PosMulMono α] [PosMulReflectLE α] (a0 : 0 < a) : a * b ≤ a ↔ b ≤ 1 :=
  Iff.trans (by rw [mul_one]) (mul_le_mul_left a0)

Inequality Equivalence Under Left Multiplication by Positive Elements: $a > 0 \implies (a \cdot b \leq a \leftrightarrow b \leq 1)$

Informal description

Let $\alpha$ be a preorder with a multiplication operation and a zero element, such that left multiplication by nonnegative elements is monotone (`PosMulMono α`) and left multiplication by positive elements reflects the non-strict order (`PosMulReflectLE α`). For any positive element $a > 0$ in $\alpha$, we have the equivalence: \[ a \cdot b \leq a \quad \text{if and only if} \quad b \leq 1. \]

mul_lt_iff_lt_one_right theorem

[PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) : a * b < a ↔ b < 1

Full source

@[simp]
theorem mul_lt_iff_lt_one_right [PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) :
    a * b < a ↔ b < 1 :=
  Iff.trans (by rw [mul_one]) (mul_lt_mul_left a0)

Strict Inequality Under Left Multiplication by Positive Elements: $a > 0 \implies (a \cdot b < a \leftrightarrow b < 1)$

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If left multiplication by positive elements is strictly monotone (`PosMulStrictMono α`) and left multiplication by nonnegative elements reflects the strict order (`PosMulReflectLT α`), then for any positive element $a > 0$ and any element $b \in \alpha$, we have the equivalence: \[ a \cdot b < a \quad \text{if and only if} \quad b < 1. \]

le_mul_iff_one_le_left theorem

[MulPosMono α] [MulPosReflectLE α] (a0 : 0 < a) : a ≤ b * a ↔ 1 ≤ b

Full source

@[simp]
lemma le_mul_iff_one_le_left [MulPosMono α] [MulPosReflectLE α] (a0 : 0 < a) : a ≤ b * a ↔ 1 ≤ b :=
  Iff.trans (by rw [one_mul]) (mul_le_mul_right a0)

Inequality Equivalence Under Right Multiplication by Positive Elements: $a > 0 \implies (a \leq b \cdot a \leftrightarrow 1 \leq b)$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where right multiplication by nonnegative elements is monotone and right multiplication by positive elements reflects the non-strict order. For any positive element $a > 0$ and any element $b \in \alpha$, we have the equivalence: \[ a \leq b \cdot a \quad \text{if and only if} \quad 1 \leq b. \]

lt_mul_iff_one_lt_left theorem

[MulPosStrictMono α] [MulPosReflectLT α] (a0 : 0 < a) : a < b * a ↔ 1 < b

Full source

@[simp]
theorem lt_mul_iff_one_lt_left [MulPosStrictMono α] [MulPosReflectLT α] (a0 : 0 < a) :
    a < b * a ↔ 1 < b :=
  Iff.trans (by rw [one_mul]) (mul_lt_mul_right a0)

Strict Inequality Under Right Multiplication by Positive Elements: $a > 0 \implies (a < b \cdot a \leftrightarrow 1 < b)$

Informal description

Let $\alpha$ be a preorder with a multiplication operation. If right multiplication by positive elements is strictly monotone and reflects the strict order, then for any positive element $a > 0$ and any element $b \in \alpha$, we have the equivalence: \[ a < b \cdot a \quad \text{if and only if} \quad 1 < b. \]

mul_le_iff_le_one_left theorem

[MulPosMono α] [MulPosReflectLE α] (b0 : 0 < b) : a * b ≤ b ↔ a ≤ 1

Full source

@[simp]
lemma mul_le_iff_le_one_left [MulPosMono α] [MulPosReflectLE α] (b0 : 0 < b) : a * b ≤ b ↔ a ≤ 1 :=
  Iff.trans (by rw [one_mul]) (mul_le_mul_right b0)

Right Multiplication by Positive Element Bounds Itself if and only if Left Factor is at Most One: $b > 0 \implies (a \cdot b \leq b \leftrightarrow a \leq 1)$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where right multiplication by nonnegative elements is monotone and right multiplication by positive elements reflects the non-strict order. Then for any positive element $b > 0$ and any element $a \in \alpha$, we have the equivalence: \[ a \cdot b \leq b \quad \text{if and only if} \quad a \leq 1. \]

mul_lt_iff_lt_one_left theorem

[MulPosStrictMono α] [MulPosReflectLT α] (b0 : 0 < b) : a * b < b ↔ a < 1

Full source

@[simp]
theorem mul_lt_iff_lt_one_left [MulPosStrictMono α] [MulPosReflectLT α] (b0 : 0 < b) :
    a * b < b ↔ a < 1 :=
  Iff.trans (by rw [one_mul]) (mul_lt_mul_right b0)

Strict Inequality Under Right Multiplication by Positive Element: $b > 0 \implies (a \cdot b < b \leftrightarrow a < 1)$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where right multiplication by positive elements is strictly monotone and reflects the strict order. Then for any positive element $b > 0$ and any element $a \in \alpha$, we have the equivalence: \[ a \cdot b < b \quad \text{if and only if} \quad a < 1. \]

mul_le_of_le_one_left theorem

[MulPosMono α] (hb : 0 ≤ b) (h : a ≤ 1) : a * b ≤ b

Full source

theorem mul_le_of_le_one_left [MulPosMono α] (hb : 0 ≤ b) (h : a ≤ 1) : a * b ≤ b := by
  simpa only [one_mul] using mul_le_mul_of_nonneg_right h hb

Nonnegative Element Multiplied by Less-Than-One Element Bounds Itself from Right: $b \geq 0 \land a \leq 1 \implies a \cdot b \leq b$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where right multiplication by nonnegative elements is monotone (i.e., `MulPosMono α` holds). Then for any nonnegative element $b \geq 0$ and any element $a \leq 1$, we have $a \cdot b \leq b$.

le_mul_of_one_le_left theorem

[MulPosMono α] (hb : 0 ≤ b) (h : 1 ≤ a) : b ≤ a * b

Full source

theorem le_mul_of_one_le_left [MulPosMono α] (hb : 0 ≤ b) (h : 1 ≤ a) : b ≤ a * b := by
  simpa only [one_mul] using mul_le_mul_of_nonneg_right h hb

Nonnegative Element Multiplied by Greater-Than-One Element Bounds Itself from Right: $b \geq 0 \land a \geq 1 \implies b \leq a \cdot b$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where right multiplication by nonnegative elements is monotone (i.e., `MulPosMono α` holds). Then for any nonnegative element $b \geq 0$ and any element $a \geq 1$, we have $b \leq a \cdot b$.

mul_le_of_le_one_right theorem

[PosMulMono α] (ha : 0 ≤ a) (h : b ≤ 1) : a * b ≤ a

Full source

theorem mul_le_of_le_one_right [PosMulMono α] (ha : 0 ≤ a) (h : b ≤ 1) : a * b ≤ a := by
  simpa only [mul_one] using mul_le_mul_of_nonneg_left h ha

Nonnegative Element Multiplied by Less-Than-One Element Bounds Itself: $a \geq 0 \land b \leq 1 \implies a \cdot b \leq a$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where left multiplication by nonnegative elements is monotone (i.e., `PosMulMono α` holds). Then for any nonnegative element $a \geq 0$ and any element $b \leq 1$, we have $a \cdot b \leq a$.

le_mul_of_one_le_right theorem

[PosMulMono α] (ha : 0 ≤ a) (h : 1 ≤ b) : a ≤ a * b

Full source

theorem le_mul_of_one_le_right [PosMulMono α] (ha : 0 ≤ a) (h : 1 ≤ b) : a ≤ a * b := by
  simpa only [mul_one] using mul_le_mul_of_nonneg_left h ha

Nonnegative Element Multiplied by Greater-Than-One Element Bounds Itself: $a \geq 0 \land b \geq 1 \implies a \leq a \cdot b$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where left multiplication by nonnegative elements is monotone (i.e., `PosMulMono α` holds). Then for any nonnegative element $a \geq 0$ and any element $b \geq 1$, we have $a \leq a \cdot b$.

mul_lt_of_lt_one_left theorem

[MulPosStrictMono α] (hb : 0 < b) (h : a < 1) : a * b < b

Full source

theorem mul_lt_of_lt_one_left [MulPosStrictMono α] (hb : 0 < b) (h : a < 1) : a * b < b := by
  simpa only [one_mul] using mul_lt_mul_of_pos_right h hb

Strict inequality under left multiplication by elements less than one: $b > 0 \land a < 1 \implies a \cdot b < b$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where right multiplication by positive elements is strictly monotone. For any positive element $b > 0$ and any element $a < 1$, we have $a \cdot b < b$.

lt_mul_of_one_lt_left theorem

[MulPosStrictMono α] (hb : 0 < b) (h : 1 < a) : b < a * b

Full source

theorem lt_mul_of_one_lt_left [MulPosStrictMono α] (hb : 0 < b) (h : 1 < a) : b < a * b := by
  simpa only [one_mul] using mul_lt_mul_of_pos_right h hb

Strict inequality under left multiplication by elements greater than one: $b > 0 \land 1 < a \implies b < a \cdot b$

Informal description

Let $\alpha$ be a preorder with a multiplication operation where right multiplication by positive elements is strictly monotone. For any positive element $b > 0$ and any element $a > 1$, we have $b < a \cdot b$.

mul_lt_of_lt_one_right theorem

[PosMulStrictMono α] (ha : 0 < a) (h : b < 1) : a * b < a

Full source

theorem mul_lt_of_lt_one_right [PosMulStrictMono α] (ha : 0 < a) (h : b < 1) : a * b < a := by
  simpa only [mul_one] using mul_lt_mul_of_pos_left h ha

Strict inequality under right multiplication by elements less than one: $a > 0 \land b < 1 \implies a \cdot b < a$

Informal description

Let $\alpha$ be a preorder with a multiplication operation such that left multiplication by positive elements is strictly monotone. For any positive element $a > 0$ and any element $b < 1$, we have $a \cdot b < a$.

lt_mul_of_one_lt_right theorem

[PosMulStrictMono α] (ha : 0 < a) (h : 1 < b) : a < a * b

Full source

theorem lt_mul_of_one_lt_right [PosMulStrictMono α] (ha : 0 < a) (h : 1 < b) : a < a * b := by
  simpa only [mul_one] using mul_lt_mul_of_pos_left h ha

Strict inequality under right multiplication by elements greater than one: $a > 0 \land 1 < b \implies a < a \cdot b$

Informal description

Let $\alpha$ be a preorder with a multiplication operation such that left multiplication by positive elements is strictly monotone. For any positive element $a > 0$ and any element $b$ with $1 < b$, we have $a < a \cdot b$.

Monotone.mul theorem

 [PosMulMono M₀] [MulPosMono M₀] (hf : Monotone f) (hg : Monotone g) (hf₀ : ∀ x, 0 ≤ f x) (hg₀ : ∀ x, 0 ≤ g x) :
  Monotone (f * g)

Full source

lemma Monotone.mul [PosMulMono M₀] [MulPosMono M₀] (hf : Monotone f) (hg : Monotone g)
    (hf₀ : ∀ x, 0 ≤ f x) (hg₀ : ∀ x, 0 ≤ g x) : Monotone (f * g) :=
  fun _ _ h ↦ mul_le_mul (hf h) (hg h) (hg₀ _) (hf₀ _)

Monotonicity of the product of nonnegative monotone functions

Informal description

Let $M₀$ be a type with multiplication and a preorder, where left multiplication by nonnegative elements is monotone (`PosMulMono`) and right multiplication by nonnegative elements is monotone (`MulPosMono`). If $f$ and $g$ are monotone functions from a type $\alpha$ to $M₀$, and $f(x) \geq 0$ and $g(x) \geq 0$ for all $x \in \alpha$, then the pointwise product function $(f \cdot g)(x) = f(x) \cdot g(x)$ is also monotone.

MonotoneOn.mul theorem

 [PosMulMono M₀] [MulPosMono M₀] {s : Set α} (hf : MonotoneOn f s) (hg : MonotoneOn g s) (hf₀ : ∀ x ∈ s, 0 ≤ f x)
  (hg₀ : ∀ x ∈ s, 0 ≤ g x) : MonotoneOn (f * g) s

Full source

lemma MonotoneOn.mul [PosMulMono M₀] [MulPosMono M₀] {s : Set α} (hf : MonotoneOn f s)
    (hg : MonotoneOn g s) (hf₀ : ∀ x ∈ s, 0 ≤ f x) (hg₀ : ∀ x ∈ s, 0 ≤ g x) :
    MonotoneOn (f * g) s :=
  fun _ ha _ hb h ↦ mul_le_mul (hf ha hb h) (hg ha hb h) (hg₀ _ ha) (hf₀ _ hb)

Monotonicity of the product of nonnegative monotone functions on a set

Informal description

Let $M₀$ be a type with multiplication and a preorder, where left multiplication by nonnegative elements is monotone (`PosMulMono`) and right multiplication by nonnegative elements is monotone (`MulPosMono`). Given a set $s \subseteq \alpha$ and functions $f, g : \alpha \to M₀$ that are monotone on $s$, with $f(x) \geq 0$ and $g(x) \geq 0$ for all $x \in s$, then the pointwise product function $(f \cdot g)(x) = f(x) \cdot g(x)$ is also monotone on $s$.

pow_nonneg theorem

[ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 0 ≤ a) : ∀ n, 0 ≤ a ^ n

Full source

@[simp] lemma pow_nonneg [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 0 ≤ a) : ∀ n, 0 ≤ a ^ n
  | 0 => pow_zero a ▸ zero_le_one
  | n + 1 => pow_succ a n ▸ mul_nonneg (pow_nonneg ha _) ha

Nonnegativity of Powers of Nonnegative Elements

Informal description

Let $M₀$ be a type with instances `ZeroLEOneClass` and `PosMulMono`. For any element $a \in M₀$ with $a \geq 0$, and for any natural number $n$, the $n$-th power of $a$ is nonnegative, i.e., $a^n \geq 0$.

zero_pow_le_one theorem

[ZeroLEOneClass M₀] : ∀ n : ℕ, (0 : M₀) ^ n ≤ 1

Full source

lemma zero_pow_le_one [ZeroLEOneClass M₀] : ∀ n : ℕ, (0 : M₀) ^ n ≤ 1
  | 0 => (pow_zero _).le
  | n + 1 => by rw [zero_pow n.succ_ne_zero]; exact zero_le_one

Zero to the Power of n is Bounded by One

Informal description

For any type $M₀$ with instances `ZeroLEOneClass` and `PosMulMono`, and for any natural number $n$, the $n$-th power of zero is less than or equal to one, i.e., $0^n \leq 1$.

pow_right_anti₀ theorem

[PosMulMono M₀] (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) : Antitone (fun n : ℕ ↦ a ^ n)

Full source

lemma pow_right_anti₀ [PosMulMono M₀] (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) : Antitone (fun n : ℕ ↦ a ^ n) :=
  antitone_nat_of_succ_le fun n ↦ by
    have : ZeroLEOneClass M₀ := ⟨ha₀.trans ha₁⟩
    rw [← mul_one (a ^ n), pow_succ]
    exact mul_le_mul_of_nonneg_left ha₁ (pow_nonneg ha₀ n)

Antitonicity of Powers for $0 \leq a \leq 1$

Informal description

Let $M₀$ be a type with a multiplication operation and a preorder, where left multiplication by nonnegative elements is monotone (i.e., `PosMulMono M₀` holds). For any element $a \in M₀$ satisfying $0 \leq a \leq 1$, the function $n \mapsto a^n$ is antitone (i.e., decreasing) with respect to the natural number $n$.

pow_le_pow_of_le_one theorem

[PosMulMono M₀] (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) {m n : ℕ} (hmn : m ≤ n) : a ^ n ≤ a ^ m

Full source

lemma pow_le_pow_of_le_one [PosMulMono M₀] (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) {m n : ℕ}
    (hmn : m ≤ n) : a ^ n ≤ a ^ m := pow_right_anti₀ ha₀ ha₁ hmn

Monotonicity of powers for $0 \leq a \leq 1$: $a^n \leq a^m$ when $m \leq n$

Informal description

Let $M₀$ be a type with multiplication and a preorder, where left multiplication by nonnegative elements is monotone. For any element $a \in M₀$ satisfying $0 \leq a \leq 1$, and for any natural numbers $m \leq n$, we have $a^n \leq a^m$.

pow_le_of_le_one theorem

[PosMulMono M₀] (h₀ : 0 ≤ a) (h₁ : a ≤ 1) (hn : n ≠ 0) : a ^ n ≤ a

Full source

lemma pow_le_of_le_one [PosMulMono M₀] (h₀ : 0 ≤ a) (h₁ : a ≤ 1) (hn : n ≠ 0) : a ^ n ≤ a :=
  (pow_one a).subst (pow_le_pow_of_le_one h₀ h₁ (Nat.pos_of_ne_zero hn))

Nonzero Power of Element Between Zero and One is At Most the Element Itself

Informal description

Let $M_0$ be a type with multiplication and a preorder, where left multiplication by nonnegative elements is monotone. For any element $a \in M_0$ satisfying $0 \leq a \leq 1$ and any nonzero natural number $n$, we have $a^n \leq a$.

sq_le theorem

[PosMulMono M₀] (h₀ : 0 ≤ a) (h₁ : a ≤ 1) : a ^ 2 ≤ a

Full source

lemma sq_le [PosMulMono M₀] (h₀ : 0 ≤ a) (h₁ : a ≤ 1) : a ^ 2 ≤ a :=
  pow_le_of_le_one h₀ h₁ two_ne_zero

Square of Element Between Zero and One is At Most the Element Itself

Informal description

Let $M_0$ be a type with multiplication and a preorder, where left multiplication by nonnegative elements is monotone. For any element $a \in M_0$ satisfying $0 \leq a \leq 1$, the square of $a$ is less than or equal to $a$, i.e., $a^2 \leq a$.

pow_le_one₀ theorem

[PosMulMono M₀] {n : ℕ} (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) : a ^ n ≤ 1

Full source

lemma pow_le_one₀ [PosMulMono M₀] {n : ℕ} (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) : a ^ n ≤ 1 :=
  pow_zero a ▸ pow_right_anti₀ ha₀ ha₁ (Nat.zero_le n)

Nonnegative Power of Element Between Zero and One is At Most One

Informal description

Let $M_0$ be a type with a multiplication operation and a preorder, where left multiplication by nonnegative elements is monotone. For any element $a \in M_0$ satisfying $0 \leq a \leq 1$ and any natural number $n$, we have $a^n \leq 1$.

one_le_mul_of_one_le_of_one_le theorem

[ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 ≤ a) (hb : 1 ≤ b) : (1 : M₀) ≤ a * b

Full source

lemma one_le_mul_of_one_le_of_one_le [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 ≤ a) (hb : 1 ≤ b) :
    (1 : M₀) ≤ a * b := ha.trans <| le_mul_of_one_le_right (zero_le_one.trans ha) hb

Product of At-Least-One Elements is At Least One

Informal description

Let $M_0$ be a type with a preorder and a multiplication operation, where $0 \leq 1$ holds and left multiplication by nonnegative elements is monotone. If $1 \leq a$ and $1 \leq b$, then $1 \leq a \cdot b$.

one_lt_mul_of_le_of_lt theorem

[ZeroLEOneClass M₀] [MulPosMono M₀] (ha : 1 ≤ a) (hb : 1 < b) : 1 < a * b

Full source

lemma one_lt_mul_of_le_of_lt [ZeroLEOneClass M₀] [MulPosMono M₀] (ha : 1 ≤ a) (hb : 1 < b) :
    1 < a * b := hb.trans_le <| le_mul_of_one_le_left (zero_le_one.trans hb.le) ha

Product of At-Least-One and Greater-Than-One Elements is Greater Than One (Right Variant)

Informal description

Let $M_0$ be a type with a preorder and a multiplication operation, where right multiplication by nonnegative elements is monotone (i.e., for any $x \geq 0$, the function $\_ \cdot x$ preserves order). If $1 \leq a$ and $1 < b$, then $1 < a \cdot b$.

one_lt_mul_of_lt_of_le theorem

[ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 < a) (hb : 1 ≤ b) : 1 < a * b

Full source

lemma one_lt_mul_of_lt_of_le [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 < a) (hb : 1 ≤ b) :
    1 < a * b := ha.trans_le <| le_mul_of_one_le_right (zero_le_one.trans ha.le) hb

Product of Greater-Than-One and At-Least-One Elements is Greater Than One (Left Variant)

Informal description

Let $M_0$ be a type with a preorder and a multiplication operation, where left multiplication by nonnegative elements is monotone (i.e., for any $x \geq 0$, the function $x \cdot \_$ preserves order). If $1 < a$ and $1 \leq b$, then $1 < a \cdot b$.

mul_lt_one_of_nonneg_of_lt_one_left theorem

[PosMulMono M₀] (ha₀ : 0 ≤ a) (ha : a < 1) (hb : b ≤ 1) : a * b < 1

Full source

lemma mul_lt_one_of_nonneg_of_lt_one_left [PosMulMono M₀] (ha₀ : 0 ≤ a) (ha : a < 1) (hb : b ≤ 1) :
    a * b < 1 := (mul_le_of_le_one_right ha₀ hb).trans_lt ha

Product of Nonnegative Less-Than-One Elements is Less Than One (Left Variant)

Informal description

Let $M₀$ be a type with a multiplication operation and a preorder, where left multiplication by nonnegative elements is monotone (i.e., `PosMulMono M₀` holds). For any elements $a, b \in M₀$ such that $0 \leq a < 1$ and $b \leq 1$, we have $a \cdot b < 1$.

mul_lt_one_of_nonneg_of_lt_one_right theorem

[MulPosMono M₀] (ha : a ≤ 1) (hb₀ : 0 ≤ b) (hb : b < 1) : a * b < 1

Full source

lemma mul_lt_one_of_nonneg_of_lt_one_right [MulPosMono M₀] (ha : a ≤ 1) (hb₀ : 0 ≤ b) (hb : b < 1) :
    a * b < 1 := (mul_le_of_le_one_left hb₀ ha).trans_lt hb

Product of Elements Bounded by One is Strictly Less Than One under Right Monotonicity

Informal description

Let $M₀$ be a type with a multiplication operation and a preorder, where right multiplication by nonnegative elements is monotone (i.e., `MulPosMono M₀` holds). For any elements $a, b \in M₀$ such that $a \leq 1$, $0 \leq b$, and $b < 1$, we have $a \cdot b < 1$.

Bound.one_lt_mul theorem

[ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] : 1 ≤ a ∧ 1 < b ∨ 1 < a ∧ 1 ≤ b → 1 < a * b

Full source

@[bound]
protected lemma Bound.one_lt_mul [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] :
    1 ≤ a ∧ 1 < b1 ≤ a ∧ 1 < b ∨ 1 < a ∧ 1 ≤ b → 1 < a * b := by
  rintro (⟨ha, hb⟩ | ⟨ha, hb⟩); exacts [one_lt_mul ha hb, one_lt_mul_of_lt_of_le ha hb]

Product of Elements Greater Than or Equal to One is Greater Than One

Informal description

Let $M_0$ be a type with a multiplication operation and a preorder, where left and right multiplication by nonnegative elements are monotone (i.e., `PosMulMono M₀` and `MulPosMono M₀` hold). For any elements $a, b \in M_0$, if either $1 \leq a$ and $1 < b$, or $1 < a$ and $1 \leq b$, then $1 < a \cdot b$.

mul_le_one₀ theorem

[MulPosMono M₀] (ha : a ≤ 1) (hb₀ : 0 ≤ b) (hb : b ≤ 1) : a * b ≤ 1

Full source

@[bound]
lemma mul_le_one₀ [MulPosMono M₀] (ha : a ≤ 1) (hb₀ : 0 ≤ b) (hb : b ≤ 1) : a * b ≤ 1 :=
  (mul_le_mul_of_nonneg_right ha hb₀).trans <| by rwa [one_mul]

Product of Elements Bounded by One is Bounded by One under Right Monotonicity

Informal description

Let $M₀$ be a type with a multiplication operation and a preorder, where right multiplication by nonnegative elements is monotone (i.e., `MulPosMono M₀` holds). For any elements $a, b \in M₀$ such that $a \leq 1$, $0 \leq b$, and $b \leq 1$, we have $a \cdot b \leq 1$.

pow_lt_one₀ theorem

[PosMulMono M₀] (h₀ : 0 ≤ a) (h₁ : a < 1) : ∀ {n : ℕ}, n ≠ 0 → a ^ n < 1

Full source

lemma pow_lt_one₀ [PosMulMono M₀] (h₀ : 0 ≤ a) (h₁ : a < 1) : ∀ {n : ℕ}, n ≠ 0 → a ^ n < 1
  | 0, h => (h rfl).elim
  | n + 1, _ => by
    rw [pow_succ']; exact mul_lt_one_of_nonneg_of_lt_one_left h₀ h₁ (pow_le_one₀ h₀ h₁.le)

Nonzero Power of Element Between Zero and One is Less Than One

Informal description

Let $M_0$ be a type with a multiplication operation and a preorder, where left multiplication by nonnegative elements is monotone. For any element $a \in M_0$ such that $0 \leq a < 1$ and any nonzero natural number $n$, we have $a^n < 1$.

pow_right_mono₀ theorem

[ZeroLEOneClass M₀] [PosMulMono M₀] (h : 1 ≤ a) : Monotone (a ^ ·)

Full source

lemma pow_right_mono₀ [ZeroLEOneClass M₀] [PosMulMono M₀] (h : 1 ≤ a) : Monotone (a ^ ·) :=
  monotone_nat_of_le_succ fun n => by
    rw [pow_succ]; exact le_mul_of_one_le_right (pow_nonneg (zero_le_one.trans h) _) h

Monotonicity of Powers of Elements Greater Than or Equal to One

Informal description

Let $M_0$ be a type with instances `ZeroLEOneClass` and `PosMulMono`. For any element $a \in M_0$ with $1 \leq a$, the function $n \mapsto a^n$ is monotone, i.e., for any natural numbers $n \leq m$, we have $a^n \leq a^m$.

one_le_pow₀ theorem

[ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 ≤ a) {n : ℕ} : 1 ≤ a ^ n

Full source

lemma one_le_pow₀ [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 ≤ a) {n : ℕ} : 1 ≤ a ^ n :=
  pow_zero a ▸ pow_right_mono₀ ha n.zero_le

Nonnegative Powers of Elements Greater Than or Equal to One Are At Least One

Informal description

Let $M_0$ be a type with instances `ZeroLEOneClass` and `PosMulMono`. For any element $a \in M_0$ with $1 \leq a$ and any natural number $n$, we have $1 \leq a^n$.

one_lt_pow₀ theorem

[ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 < a) : ∀ {n : ℕ}, n ≠ 0 → 1 < a ^ n

Full source

lemma one_lt_pow₀ [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 < a) : ∀ {n : ℕ}, n ≠ 0 → 1 < a ^ n
  | 0, h => (h rfl).elim
  | n + 1, _ => by rw [pow_succ']; exact one_lt_mul_of_lt_of_le ha (one_le_pow₀ ha.le)

Powers of Elements Greater Than One Are Greater Than One: $1 < a^n$ when $1 < a$ and $n \neq 0$

Informal description

Let $M_0$ be a type with instances `ZeroLEOneClass` and `PosMulMono`. For any element $a \in M_0$ with $1 < a$ and any nonzero natural number $n$, we have $1 < a^n$.

Bound.pow_le_pow_right_of_le_one_or_one_le theorem

[ZeroLEOneClass M₀] [PosMulMono M₀] (h : 1 ≤ a ∧ n ≤ m ∨ 0 ≤ a ∧ a ≤ 1 ∧ m ≤ n) : a ^ n ≤ a ^ m

Full source

/-- `bound` lemma for branching on `1 ≤ a ∨ a ≤ 1` when proving `a ^ n ≤ a ^ m` -/
@[bound]
lemma Bound.pow_le_pow_right_of_le_one_or_one_le [ZeroLEOneClass M₀] [PosMulMono M₀]
    (h : 1 ≤ a ∧ n ≤ m1 ≤ a ∧ n ≤ m ∨ 0 ≤ a ∧ a ≤ 1 ∧ m ≤ n) :
    a ^ n ≤ a ^ m := by
  obtain ⟨a1, nm⟩ | ⟨a0, a1, mn⟩ := h
  · exact pow_right_mono₀ a1 nm
  · exact pow_le_pow_of_le_one a0 a1 mn

Monotonicity of Powers: $a^n \leq a^m$ for $a \geq 1$ and $n \leq m$ or $0 \leq a \leq 1$ and $m \leq n$

Informal description

Let $M_0$ be a type with instances `ZeroLEOneClass` and `PosMulMono`. For any element $a \in M_0$ and natural numbers $m, n$, if either: 1. $1 \leq a$ and $n \leq m$, or 2. $0 \leq a \leq 1$ and $m \leq n$, then $a^n \leq a^m$.

pow_le_pow_right₀ theorem

[ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 ≤ a) (hmn : m ≤ n) : a ^ m ≤ a ^ n

Full source

@[gcongr]
lemma pow_le_pow_right₀ [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 ≤ a) (hmn : m ≤ n) :
    a ^ m ≤ a ^ n :=
  pow_right_mono₀ ha hmn

Monotonicity of Powers for $a \geq 1$: $a^m \leq a^n$ when $m \leq n$

Informal description

Let $M_0$ be a type with instances `ZeroLEOneClass` and `PosMulMono`. For any element $a \in M_0$ such that $1 \leq a$, and for any natural numbers $m \leq n$, we have $a^m \leq a^n$.

le_self_pow₀ theorem

[ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 ≤ a) (hn : n ≠ 0) : a ≤ a ^ n

Full source

lemma le_self_pow₀ [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 ≤ a) (hn : n ≠ 0) : a ≤ a ^ n := by
  simpa only [pow_one] using pow_le_pow_right₀ ha <| Nat.pos_iff_ne_zero.2 hn

Nonnegative Element Raised to Nonzero Power is Greater Than or Equal to Itself When $a \geq 1$

Informal description

Let $M_0$ be a type with instances `ZeroLEOneClass` and `PosMulMono`. For any element $a \in M_0$ such that $1 \leq a$, and for any natural number $n \neq 0$, we have $a \leq a^n$.

Bound.le_self_pow_of_pos theorem

[ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 ≤ a) (hn : 0 < n) : a ≤ a ^ n

Full source

/-- The `bound` tactic can't handle `m ≠ 0` goals yet, so we express as `0 < m` -/
@[bound]
lemma Bound.le_self_pow_of_pos [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 ≤ a) (hn : 0 < n) :
    a ≤ a ^ n := le_self_pow₀ ha hn.ne'

Nonnegative Element Raised to Positive Power is Greater Than or Equal to Itself When $a \geq 1$

Informal description

Let $M_0$ be a type with instances `ZeroLEOneClass` and `PosMulMono`. For any element $a \in M_0$ such that $1 \leq a$, and for any natural number $n > 0$, we have $a \leq a^n$.

pow_le_pow_left₀ theorem

[ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : 0 ≤ a) (hab : a ≤ b) : ∀ n, a ^ n ≤ b ^ n

Full source

@[mono, gcongr, bound]
theorem pow_le_pow_left₀ [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀]
    (ha : 0 ≤ a) (hab : a ≤ b) : ∀ n, a ^ n ≤ b ^ n
  | 0 => by simp
  | n + 1 => by simpa only [pow_succ']
      using mul_le_mul hab (pow_le_pow_left₀ ha hab _) (pow_nonneg ha _) (ha.trans hab)

Monotonicity of Powers for Nonnegative Elements: $a^n \leq b^n$ when $0 \leq a \leq b$

Informal description

Let $M_0$ be a type with instances `ZeroLEOneClass`, `PosMulMono`, and `MulPosMono`. For any elements $a, b \in M_0$ with $0 \leq a \leq b$, and for any natural number $n$, we have $a^n \leq b^n$.

pow_left_monotoneOn theorem

[ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] : MonotoneOn (fun a : M₀ ↦ a ^ n) {x | 0 ≤ x}

Full source

lemma pow_left_monotoneOn [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] :
    MonotoneOn (fun a : M₀ ↦ a ^ n) {x | 0 ≤ x} :=
  fun _a ha _b _ hab ↦ pow_le_pow_left₀ ha hab _

Monotonicity of Power Function on Nonnegative Elements

Informal description

Let $M_0$ be a type with instances `ZeroLEOneClass`, `PosMulMono`, and `MulPosMono`. The function $a \mapsto a^n$ is monotone on the set of nonnegative elements $\{x \in M_0 \mid 0 \leq x\}$.

monotone_mul_left_of_nonneg theorem

[PosMulMono M₀] (ha : 0 ≤ a) : Monotone fun x ↦ a * x

Full source

lemma monotone_mul_left_of_nonneg [PosMulMono M₀] (ha : 0 ≤ a) : Monotone fun x ↦ a * x :=
  fun _ _ h ↦ mul_le_mul_of_nonneg_left h ha

Monotonicity of Left Multiplication by Nonnegative Elements: $x \mapsto a \cdot x$

Informal description

Let $M_0$ be a type with a multiplication operation and a preorder, such that left multiplication by nonnegative elements is monotone (i.e., `PosMulMono M₀` holds). Then for any nonnegative element $a \geq 0$, the function $x \mapsto a \cdot x$ is monotone.

monotone_mul_right_of_nonneg theorem

[MulPosMono M₀] (ha : 0 ≤ a) : Monotone fun x ↦ x * a

Full source

lemma monotone_mul_right_of_nonneg [MulPosMono M₀] (ha : 0 ≤ a) : Monotone fun x ↦ x * a :=
  fun _ _ h ↦ mul_le_mul_of_nonneg_right h ha

Monotonicity of Right Multiplication by Nonnegative Elements

Informal description

Let $M₀$ be a type with a multiplication operation and a preorder, such that right multiplication by nonnegative elements is monotone (i.e., `MulPosMono M₀` holds). Then for any nonnegative element $a \geq 0$, the function $x \mapsto x * a$ is monotone.

Monotone.mul_const theorem

[MulPosMono M₀] (hf : Monotone f) (ha : 0 ≤ a) : Monotone fun x ↦ f x * a

Full source

lemma Monotone.mul_const [MulPosMono M₀] (hf : Monotone f) (ha : 0 ≤ a) :
    Monotone fun x ↦ f x * a := (monotone_mul_right_of_nonneg ha).comp hf

Monotonicity of Right Multiplication by Nonnegative Elements Composed with Monotone Function

Informal description

Let $M₀$ be a type with a multiplication operation and a preorder, such that right multiplication by nonnegative elements is monotone (i.e., `MulPosMono M₀` holds). If $f$ is a monotone function and $a \geq 0$, then the function $x \mapsto f(x) \cdot a$ is also monotone.

Monotone.const_mul theorem

[PosMulMono M₀] (hf : Monotone f) (ha : 0 ≤ a) : Monotone fun x ↦ a * f x

Full source

lemma Monotone.const_mul [PosMulMono M₀] (hf : Monotone f) (ha : 0 ≤ a) :
    Monotone fun x ↦ a * f x := (monotone_mul_left_of_nonneg ha).comp hf

Monotonicity of Left Multiplication by Nonnegative Elements Composed with Monotone Function

Informal description

Let $M_0$ be a type with a multiplication operation and a preorder, such that left multiplication by nonnegative elements is monotone (i.e., `PosMulMono M₀` holds). If $f$ is a monotone function and $a \geq 0$, then the function $x \mapsto a \cdot f(x)$ is also monotone.

Antitone.mul_const theorem

[MulPosMono M₀] (hf : Antitone f) (ha : 0 ≤ a) : Antitone fun x ↦ f x * a

Full source

lemma Antitone.mul_const [MulPosMono M₀] (hf : Antitone f) (ha : 0 ≤ a) :
    Antitone fun x ↦ f x * a := (monotone_mul_right_of_nonneg ha).comp_antitone hf

Antitonicity of Right Multiplication by Nonnegative Elements Composed with Antitone Function

Informal description

Let $M_0$ be a type with a multiplication operation and a preorder, such that right multiplication by nonnegative elements is monotone (i.e., `MulPosMono M₀` holds). If $f$ is an antitone function and $a \geq 0$, then the function $x \mapsto f(x) \cdot a$ is also antitone.

Antitone.const_mul theorem

[PosMulMono M₀] (hf : Antitone f) (ha : 0 ≤ a) : Antitone fun x ↦ a * f x

Full source

lemma Antitone.const_mul [PosMulMono M₀] (hf : Antitone f) (ha : 0 ≤ a) :
    Antitone fun x ↦ a * f x := (monotone_mul_left_of_nonneg ha).comp_antitone hf

Antitonicity of Left Multiplication by Nonnegative Elements Composed with Antitone Function

Informal description

Let $M_0$ be a type with a multiplication operation and a preorder, such that left multiplication by nonnegative elements is monotone (i.e., `PosMulMono M₀` holds). If $f$ is an antitone function and $a \geq 0$, then the function $x \mapsto a \cdot f(x)$ is also antitone.

mul_self_lt_mul_self theorem

[PosMulStrictMono M₀] [MulPosMono M₀] (ha : 0 ≤ a) (hab : a < b) : a * a < b * b

Full source

lemma mul_self_lt_mul_self [PosMulStrictMono M₀] [MulPosMono M₀] (ha : 0 ≤ a) (hab : a < b) :
    a * a < b * b := mul_lt_mul' hab.le hab ha <| ha.trans_lt hab

Square preserves strict inequality for nonnegative elements

Informal description

Let $M_0$ be a type with a multiplication operation and a preorder, such that left multiplication by positive elements is strictly monotone and right multiplication by nonnegative elements is monotone. For any elements $a, b \in M_0$ with $0 \leq a$ and $a < b$, we have $a \cdot a < b \cdot b$.

strictMonoOn_mul_self theorem

[PosMulStrictMono M₀] [MulPosMono M₀] : StrictMonoOn (fun x ↦ x * x) {x : M₀ | 0 ≤ x}

Full source

lemma strictMonoOn_mul_self [PosMulStrictMono M₀] [MulPosMono M₀] :
    StrictMonoOn (fun x ↦ x * x) {x : M₀ | 0 ≤ x} := fun _ hx _ _ hxy ↦ mul_self_lt_mul_self hx hxy

Strict Monotonicity of Squaring on Nonnegative Elements

Informal description

Let $M_0$ be a type with a multiplication operation and a preorder, such that left multiplication by positive elements is strictly monotone and right multiplication by nonnegative elements is monotone. Then the function $x \mapsto x \cdot x$ is strictly increasing on the set of nonnegative elements $\{x \in M_0 \mid 0 \leq x\}$.

Decidable.mul_lt_mul'' theorem

 [PosMulMono M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] [DecidableLE M₀] (h1 : a < c) (h2 : b < d) (h3 : 0 ≤ a)
  (h4 : 0 ≤ b) : a * b < c * d

Full source

protected lemma Decidable.mul_lt_mul'' [PosMulMono M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀]
    [DecidableLE M₀] (h1 : a < c) (h2 : b < d) (h3 : 0 ≤ a) (h4 : 0 ≤ b) : a * b < c * d :=
  h4.lt_or_eq_dec.elim (fun b0 ↦ mul_lt_mul h1 h2.le b0 <| h3.trans h1.le) fun b0 ↦ by
    rw [← b0, mul_zero]; exact mul_pos (h3.trans_lt h1) (h4.trans_lt h2)

Strict inequality for products under componentwise comparison: $a < c \land b < d \land a \geq 0 \land b \geq 0 \implies a \cdot b < c \cdot d$

Informal description

Let $M₀$ be a preorder with a multiplication operation such that: 1. Left multiplication by nonnegative elements is monotone 2. Left multiplication by positive elements is strictly monotone 3. Right multiplication by positive elements is strictly monotone 4. The order relation is decidable For any elements $a, b, c, d \in M₀$ with $a < c$, $b < d$, $0 \leq a$, and $0 \leq b$, we have $a \cdot b < c \cdot d$.

lt_mul_left theorem

[MulPosStrictMono M₀] (ha : 0 < a) (hb : 1 < b) : a < b * a

Full source

lemma lt_mul_left [MulPosStrictMono M₀] (ha : 0 < a) (hb : 1 < b) : a < b * a := by
  simpa using mul_lt_mul_of_pos_right hb ha

Strict inequality under right multiplication: $a > 0 \land b > 1 \implies a < b \cdot a$

Informal description

Let $M₀$ be a preorder with a multiplication operation such that right multiplication by positive elements is strictly monotone. For any elements $a, b \in M₀$ with $a > 0$ and $b > 1$, we have $a < b \cdot a$.

lt_mul_right theorem

[PosMulStrictMono M₀] (ha : 0 < a) (hb : 1 < b) : a < a * b

Full source

lemma lt_mul_right [PosMulStrictMono M₀] (ha : 0 < a) (hb : 1 < b) : a < a * b := by
  simpa using mul_lt_mul_of_pos_left hb ha

Strict inequality under left multiplication: $a > 0 \land b > 1 \implies a < a \cdot b$

Informal description

Let $M₀$ be a preorder with a multiplication operation such that left multiplication by positive elements is strictly monotone. For any elements $a, b \in M₀$ with $a > 0$ and $b > 1$, we have $a < a \cdot b$.

lt_mul_self theorem

[ZeroLEOneClass M₀] [MulPosStrictMono M₀] (ha : 1 < a) : a < a * a

Full source

lemma lt_mul_self [ZeroLEOneClass M₀] [MulPosStrictMono M₀] (ha : 1 < a) : a < a * a :=
  lt_mul_left (ha.trans_le' zero_le_one) ha

Strict inequality for self-multiplication: $1 < a \implies a < a^2$

Informal description

Let $M₀$ be a preorder with a multiplication operation such that $0 \leq 1$ and right multiplication by positive elements is strictly monotone. For any element $a \in M₀$ with $1 < a$, we have $a < a \cdot a$.

sq_pos_of_pos theorem

[PosMulStrictMono M₀] (ha : 0 < a) : 0 < a ^ 2

Full source

lemma sq_pos_of_pos [PosMulStrictMono M₀] (ha : 0 < a) : 0 < a ^ 2 := by
  simpa only [sq] using mul_pos ha ha

Positivity of squares for positive elements in strictly monotone left multiplication preorders

Informal description

Let $M₀$ be a preorder with a multiplication operation such that left multiplication by positive elements is strictly monotone. For any positive element $a \in M₀$ (i.e., $0 < a$), the square of $a$ is also positive, i.e., $0 < a^2$.

pow_pos theorem

(ha : 0 < a) : ∀ n, 0 < a ^ n

Full source

@[simp] lemma pow_pos (ha : 0 < a) : ∀ n, 0 < a ^ n
  | 0 => by nontriviality; rw [pow_zero]; exact zero_lt_one
  | _ + 1 => pow_succ a _ ▸ mul_pos (pow_pos ha _) ha

Positivity of Powers: $a > 0 \implies a^n > 0$ for all $n \in \mathbb{N}$

Informal description

For any positive element $a > 0$ in a preorder $M_0$ with a multiplication operation, and for any natural number $n$, the $n$-th power of $a$ is positive, i.e., $a^n > 0$.

pow_lt_pow_left₀ theorem

[MulPosMono M₀] (hab : a < b) (ha : 0 ≤ a) : ∀ {n : ℕ}, n ≠ 0 → a ^ n < b ^ n

Full source

@[gcongr, bound]
lemma pow_lt_pow_left₀ [MulPosMono M₀] (hab : a < b)
    (ha : 0 ≤ a) : ∀ {n : ℕ}, n ≠ 0 → a ^ n < b ^ n
  | n + 1, _ => by
    simpa only [pow_succ] using mul_lt_mul_of_le_of_lt_of_nonneg_of_pos
      (pow_le_pow_left₀ ha hab.le _) hab ha (pow_pos (ha.trans_lt hab) _)

Strict Monotonicity of Powers for Nonnegative Elements: $a < b \land a \geq 0 \implies a^n < b^n$ for $n \neq 0$

Informal description

Let $M_0$ be a preorder with a multiplication operation such that right multiplication by nonnegative elements is monotone (`MulPosMono M_0`). For any elements $a, b \in M_0$ with $a < b$ and $a \geq 0$, and for any nonzero natural number $n$, we have $a^n < b^n$.

pow_left_strictMonoOn₀ theorem

[MulPosMono M₀] (hn : n ≠ 0) : StrictMonoOn (· ^ n : M₀ → M₀) {a | 0 ≤ a}

Full source

/-- See also `pow_left_strictMono₀` and `Nat.pow_left_strictMono`. -/
lemma pow_left_strictMonoOn₀ [MulPosMono M₀] (hn : n ≠ 0) :
    StrictMonoOn (· ^ n : M₀ → M₀) {a | 0 ≤ a} :=
  fun _a ha _b _ hab ↦ pow_lt_pow_left₀ hab ha hn

Strict Monotonicity of Power Function on Nonnegative Elements for $n \neq 0$

Informal description

Let $M_0$ be a preorder with a multiplication operation such that right multiplication by nonnegative elements is monotone (`MulPosMono M_0`). For any nonzero natural number $n$, the function $a \mapsto a^n$ is strictly increasing on the set of nonnegative elements $\{a \in M_0 \mid 0 \leq a\}$.

pow_right_strictMono₀ theorem

(h : 1 < a) : StrictMono (a ^ ·)

Full source

/-- See also `pow_right_strictMono'`. -/
lemma pow_right_strictMono₀ (h : 1 < a) : StrictMono (a ^ ·) :=
  strictMono_nat_of_lt_succ fun n => by
    simpa only [one_mul, pow_succ] using lt_mul_right (pow_pos (zero_le_one.trans_lt h) _) h

Strict Monotonicity of Powers: $a > 1 \implies n \mapsto a^n$ is strictly increasing

Informal description

For any element $a > 1$ in a preorder $M_0$ with a multiplication operation, the function $n \mapsto a^n$ is strictly increasing on natural numbers.

pow_lt_pow_right₀ theorem

(h : 1 < a) (hmn : m < n) : a ^ m < a ^ n

Full source

@[gcongr]
lemma pow_lt_pow_right₀ (h : 1 < a) (hmn : m < n) : a ^ m < a ^ n := pow_right_strictMono₀ h hmn

Strict Monotonicity of Powers: $a > 1 \implies a^m < a^n$ for $m < n$

Informal description

For any element $a > 1$ in a preordered multiplicative structure and natural numbers $m < n$, we have $a^m < a^n$.

pow_lt_pow_iff_right₀ theorem

(h : 1 < a) : a ^ n < a ^ m ↔ n < m

Full source

lemma pow_lt_pow_iff_right₀ (h : 1 < a) : a ^ n < a ^ m ↔ n < m :=
  (pow_right_strictMono₀ h).lt_iff_lt

Strict Monotonicity of Powers: $a^n < a^m \leftrightarrow n < m$ for $a > 1$

Informal description

For any element $a > 1$ in a preorder $M_0$ with a multiplication operation, and for any natural numbers $n$ and $m$, we have $a^n < a^m$ if and only if $n < m$.

pow_le_pow_iff_right₀ theorem

(h : 1 < a) : a ^ n ≤ a ^ m ↔ n ≤ m

Full source

lemma pow_le_pow_iff_right₀ (h : 1 < a) : a ^ n ≤ a ^ m ↔ n ≤ m :=
  (pow_right_strictMono₀ h).le_iff_le

Power Inequality Comparison for $a > 1$: $a^n \leq a^m \leftrightarrow n \leq m$

Informal description

For any element $a > 1$ in a preorder with multiplication, the inequality $a^n \leq a^m$ holds if and only if $n \leq m$ for natural numbers $n$ and $m$.

lt_self_pow₀ theorem

(h : 1 < a) (hm : 1 < m) : a < a ^ m

Full source

lemma lt_self_pow₀ (h : 1 < a) (hm : 1 < m) : a < a ^ m := by
  simpa only [pow_one] using pow_lt_pow_right₀ h hm

Strict Inequality for Powers: $a < a^m$ when $a > 1$ and $m > 1$

Informal description

For any element $a > 1$ in a preordered multiplicative structure and any natural number $m > 1$, we have $a < a^m$.

pow_right_strictAnti₀ theorem

(h₀ : 0 < a) (h₁ : a < 1) : StrictAnti (a ^ ·)

Full source

lemma pow_right_strictAnti₀ (h₀ : 0 < a) (h₁ : a < 1) : StrictAnti (a ^ ·) :=
  strictAnti_nat_of_succ_lt fun n => by
    simpa only [pow_succ, mul_one] using mul_lt_mul_of_pos_left h₁ (pow_pos h₀ n)

Strict Antitonicity of Powers for $0 < a < 1$

Informal description

For any element $a$ in a preorder with a multiplication operation, if $0 < a < 1$, then the function $n \mapsto a^n$ is strictly antitone (i.e., for any natural numbers $m < n$, we have $a^n < a^m$).

pow_lt_pow_iff_right_of_lt_one₀ theorem

(h₀ : 0 < a) (h₁ : a < 1) : a ^ m < a ^ n ↔ n < m

Full source

lemma pow_lt_pow_iff_right_of_lt_one₀ (h₀ : 0 < a) (h₁ : a < 1) : a ^ m < a ^ n ↔ n < m :=
  (pow_right_strictAnti₀ h₀ h₁).lt_iff_lt

Inequality for Powers with Base $0 < a < 1$: $a^m < a^n \leftrightarrow n < m$

Informal description

For any element $a$ in a preorder with a multiplication operation, if $0 < a < 1$, then the inequality $a^m < a^n$ holds if and only if $n < m$.

pow_lt_pow_right_of_lt_one₀ theorem

(h₀ : 0 < a) (h₁ : a < 1) (hmn : m < n) : a ^ n < a ^ m

Full source

lemma pow_lt_pow_right_of_lt_one₀ (h₀ : 0 < a) (h₁ : a < 1) (hmn : m < n) : a ^ n < a ^ m :=
  (pow_lt_pow_iff_right_of_lt_one₀ h₀ h₁).2 hmn

Strict Antitonicity of Powers for $0 < a < 1$: $a^n < a^m$ when $m < n$

Informal description

For any element $a$ in a preordered type with multiplication and zero, if $0 < a < 1$ and $m < n$ are natural numbers, then $a^n < a^m$.

pow_lt_self_of_lt_one₀ theorem

(h₀ : 0 < a) (h₁ : a < 1) (hn : 1 < n) : a ^ n < a

Full source

lemma pow_lt_self_of_lt_one₀ (h₀ : 0 < a) (h₁ : a < 1) (hn : 1 < n) : a ^ n < a := by
  simpa only [pow_one] using pow_lt_pow_right_of_lt_one₀ h₀ h₁ hn

Strict Antitonicity of Powers for $0 < a < 1$: $a^n < a$ when $n > 1$

Informal description

For any element $a$ in a preordered type with multiplication and zero, if $0 < a < 1$ and $n > 1$ is a natural number, then $a^n < a$.

strictMono_mul_left_of_pos theorem

[PosMulStrictMono M₀] (ha : 0 < a) : StrictMono fun x ↦ a * x

Full source

lemma strictMono_mul_left_of_pos [PosMulStrictMono M₀] (ha : 0 < a) :
    StrictMono fun x ↦ a * x := fun _ _ b_lt_c ↦ mul_lt_mul_of_pos_left b_lt_c ha

Strict monotonicity of left multiplication by positive elements

Informal description

Let $M₀$ be a preordered type with multiplication and zero, where left multiplication by positive elements is strictly monotone (i.e., `PosMulStrictMono M₀` holds). Then for any $a > 0$ in $M₀$, the function $x \mapsto a \cdot x$ is strictly increasing.

strictMono_mul_right_of_pos theorem

[MulPosStrictMono M₀] (ha : 0 < a) : StrictMono fun x ↦ x * a

Full source

lemma strictMono_mul_right_of_pos [MulPosStrictMono M₀] (ha : 0 < a) :
    StrictMono fun x ↦ x * a := fun _ _ b_lt_c ↦ mul_lt_mul_of_pos_right b_lt_c ha

Strict Monotonicity of Right Multiplication by Positive Elements: $x \mapsto x \cdot a$ is strictly increasing for $a > 0$

Informal description

Let $M_0$ be a preordered type with multiplication and zero, where right multiplication by positive elements is strictly monotone (i.e., the typeclass `MulPosStrictMono M₀` holds). Then for any positive element $a > 0$ in $M_0$, the function $x \mapsto x \cdot a$ is strictly increasing.

StrictMono.mul_const theorem

[MulPosStrictMono M₀] (hf : StrictMono f) (ha : 0 < a) : StrictMono fun x ↦ f x * a

Full source

lemma StrictMono.mul_const [MulPosStrictMono M₀] (hf : StrictMono f) (ha : 0 < a) :
    StrictMono fun x ↦ f x * a := (strictMono_mul_right_of_pos ha).comp hf

Strictly Increasing Function Composed with Right Multiplication by Positive Element is Strictly Increasing

Informal description

Let $M_0$ be a preordered type with multiplication and zero, where right multiplication by positive elements is strictly monotone (i.e., the typeclass `MulPosStrictMono M₀` holds). If $f$ is a strictly increasing function and $a > 0$ is a positive element in $M_0$, then the function $x \mapsto f(x) \cdot a$ is strictly increasing.

StrictMono.const_mul theorem

[PosMulStrictMono M₀] (hf : StrictMono f) (ha : 0 < a) : StrictMono fun x ↦ a * f x

Full source

lemma StrictMono.const_mul [PosMulStrictMono M₀] (hf : StrictMono f) (ha : 0 < a) :
    StrictMono fun x ↦ a * f x := (strictMono_mul_left_of_pos ha).comp hf

Strictly Increasing Function Composed with Left Multiplication by Positive Element is Strictly Increasing

Informal description

Let $M_0$ be a preordered type with multiplication and zero, where left multiplication by positive elements is strictly monotone (i.e., the typeclass `PosMulStrictMono M₀` holds). If $f$ is a strictly increasing function and $a > 0$ is a positive element in $M_0$, then the function $x \mapsto a \cdot f(x)$ is strictly increasing.

StrictAnti.mul_const theorem

[MulPosStrictMono M₀] (hf : StrictAnti f) (ha : 0 < a) : StrictAnti fun x ↦ f x * a

Full source

lemma StrictAnti.mul_const [MulPosStrictMono M₀] (hf : StrictAnti f) (ha : 0 < a) :
    StrictAnti fun x ↦ f x * a := (strictMono_mul_right_of_pos ha).comp_strictAnti hf

Strictly Decreasing Function Composed with Right Multiplication by Positive Element is Strictly Decreasing

Informal description

Let $M_0$ be a preordered type with multiplication and zero, where right multiplication by positive elements is strictly monotone (i.e., the typeclass `MulPosStrictMono M₀` holds). If $f$ is a strictly decreasing function and $a > 0$ is a positive element in $M_0$, then the function $x \mapsto f(x) \cdot a$ is strictly decreasing.

StrictAnti.const_mul theorem

[PosMulStrictMono M₀] (hf : StrictAnti f) (ha : 0 < a) : StrictAnti fun x ↦ a * f x

Full source

lemma StrictAnti.const_mul [PosMulStrictMono M₀] (hf : StrictAnti f) (ha : 0 < a) :
    StrictAnti fun x ↦ a * f x := (strictMono_mul_left_of_pos ha).comp_strictAnti hf

Strictly Decreasing Function Composed with Left Multiplication by Positive Element is Strictly Decreasing

Informal description

Let $M_0$ be a preordered type with multiplication and zero, where left multiplication by positive elements is strictly monotone (i.e., the typeclass `PosMulStrictMono M₀` holds). If $f$ is a strictly decreasing function and $a > 0$ is a positive element in $M_0$, then the function $x \mapsto a \cdot f(x)$ is strictly decreasing.

StrictMono.mul_monotone theorem

 [PosMulMono M₀] [MulPosStrictMono M₀] (hf : StrictMono f) (hg : Monotone g) (hf₀ : ∀ x, 0 ≤ f x) (hg₀ : ∀ x, 0 < g x) :
  StrictMono (f * g)

Full source

lemma StrictMono.mul_monotone [PosMulMono M₀] [MulPosStrictMono M₀] (hf : StrictMono f)
    (hg : Monotone g) (hf₀ : ∀ x, 0 ≤ f x) (hg₀ : ∀ x, 0 < g x) :
    StrictMono (f * g) := fun _ _ h ↦ mul_lt_mul (hf h) (hg h.le) (hg₀ _) (hf₀ _)

Strictly Increasing Function Multiplied by Monotone Positive Function is Strictly Increasing

Informal description

Let $M_0$ be a preordered type with multiplication and zero, where left multiplication by nonnegative elements is monotone (i.e., `PosMulMono M₀` holds) and right multiplication by positive elements is strictly monotone (i.e., `MulPosStrictMono M₀` holds). If $f$ is a strictly increasing function with $f(x) \geq 0$ for all $x$, and $g$ is a monotone function with $g(x) > 0$ for all $x$, then the pointwise product function $f \cdot g$ is strictly increasing.

Monotone.mul_strictMono theorem

 [PosMulStrictMono M₀] [MulPosMono M₀] (hf : Monotone f) (hg : StrictMono g) (hf₀ : ∀ x, 0 < f x) (hg₀ : ∀ x, 0 ≤ g x) :
  StrictMono (f * g)

Full source

lemma Monotone.mul_strictMono [PosMulStrictMono M₀] [MulPosMono M₀] (hf : Monotone f)
    (hg : StrictMono g) (hf₀ : ∀ x, 0 < f x) (hg₀ : ∀ x, 0 ≤ g x) :
    StrictMono (f * g) := fun _ _ h ↦ mul_lt_mul' (hf h.le) (hg h) (hg₀ _) (hf₀ _)

Product of Monotone and Strictly Monotone Nonnegative Functions is Strictly Monotone

Informal description

Let $M_0$ be a preordered type with multiplication and zero, where left multiplication by positive elements is strictly monotone (`PosMulStrictMono M₀`) and right multiplication by nonnegative elements is monotone (`MulPosMono M₀`). If $f$ is a monotone function with $f(x) > 0$ for all $x$, and $g$ is a strictly monotone function with $g(x) \geq 0$ for all $x$, then the pointwise product function $f \cdot g$ is strictly monotone.

StrictMono.mul theorem

 [PosMulStrictMono M₀] [MulPosStrictMono M₀] (hf : StrictMono f) (hg : StrictMono g) (hf₀ : ∀ x, 0 ≤ f x)
  (hg₀ : ∀ x, 0 ≤ g x) : StrictMono (f * g)

Full source

lemma StrictMono.mul [PosMulStrictMono M₀] [MulPosStrictMono M₀] (hf : StrictMono f)
    (hg : StrictMono g) (hf₀ : ∀ x, 0 ≤ f x) (hg₀ : ∀ x, 0 ≤ g x) :
    StrictMono (f * g) := fun _ _ h ↦ mul_lt_mul'' (hf h) (hg h) (hf₀ _) (hg₀ _)

Strict Monotonicity of the Product of Nonnegative Strictly Monotone Functions

Informal description

Let $M₀$ be a preorder where left multiplication by positive elements is strictly monotone (`PosMulStrictMono`) and right multiplication by positive elements is strictly monotone (`MulPosStrictMono`). If $f$ and $g$ are strictly monotone functions such that $f(x) \geq 0$ and $g(x) \geq 0$ for all $x$, then the pointwise product function $f \cdot g$ is also strictly monotone.

pow_le_pow_iff_left₀ theorem

[MulPosMono M₀] (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) : a ^ n ≤ b ^ n ↔ a ≤ b

Full source

lemma pow_le_pow_iff_left₀ [MulPosMono M₀] (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) :
    a ^ n ≤ b ^ n ↔ a ≤ b :=
  (pow_left_strictMonoOn₀ hn).le_iff_le ha hb

Power Inequality Equivalence for Nonnegative Elements: $a^n \leq b^n \leftrightarrow a \leq b$ when $n \neq 0$

Informal description

Let $M_0$ be a preorder where right multiplication by nonnegative elements is monotone (`MulPosMono M₀`). For any nonnegative elements $a, b \in M_0$ with $0 \leq a$ and $0 \leq b$, and any nonzero natural number $n$, we have $a^n \leq b^n$ if and only if $a \leq b$.

pow_lt_pow_iff_left₀ theorem

[MulPosMono M₀] (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) : a ^ n < b ^ n ↔ a < b

Full source

lemma pow_lt_pow_iff_left₀ [MulPosMono M₀] (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) :
    a ^ n < b ^ n ↔ a < b :=
  (pow_left_strictMonoOn₀ hn).lt_iff_lt ha hb

Strict Monotonicity of Power Function on Nonnegative Elements: $a^n < b^n \leftrightarrow a < b$ for $n \neq 0$

Informal description

Let $M_0$ be a preorder where right multiplication by nonnegative elements is monotone (`MulPosMono M_0`). For any nonnegative elements $a, b \in M_0$ with $0 \leq a$ and $0 \leq b$, and any nonzero natural number $n \neq 0$, we have $a^n < b^n$ if and only if $a < b$.

pow_left_inj₀ theorem

[MulPosMono M₀] (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b

Full source

@[simp]
lemma pow_left_inj₀ [MulPosMono M₀] (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) :
    a ^ n = b ^ n ↔ a = b :=
  (pow_left_strictMonoOn₀ hn).eq_iff_eq ha hb

Injectivity of Power Function on Nonnegative Elements: $a^n = b^n \leftrightarrow a = b$ for $n \neq 0$

Informal description

Let $M_0$ be a preorder with a multiplication operation such that right multiplication by nonnegative elements is monotone. For any nonnegative elements $a, b \in M_0$ and any nonzero natural number $n$, the equality $a^n = b^n$ holds if and only if $a = b$.

pow_right_injective₀ theorem

(ha₀ : 0 < a) (ha₁ : a ≠ 1) : Injective (a ^ ·)

Full source

lemma pow_right_injective₀ (ha₀ : 0 < a) (ha₁ : a ≠ 1) : Injective (a ^ ·) := by
  obtain ha₁ | ha₁ := ha₁.lt_or_lt
  · exact (pow_right_strictAnti₀ ha₀ ha₁).injective
  · exact (pow_right_strictMono₀ ha₁).injective

Injectivity of Power Function for $0 < a \neq 1$

Informal description

For any element $a > 0$ with $a \neq 1$ in a preorder with a multiplication operation, the power function $n \mapsto a^n$ is injective on natural numbers. That is, for any natural numbers $m$ and $n$, if $a^m = a^n$, then $m = n$.

pow_right_inj₀ theorem

(ha₀ : 0 < a) (ha₁ : a ≠ 1) : a ^ m = a ^ n ↔ m = n

Full source

@[simp]
lemma pow_right_inj₀ (ha₀ : 0 < a) (ha₁ : a ≠ 1) : a ^ m = a ^ n ↔ m = n :=
  (pow_right_injective₀ ha₀ ha₁).eq_iff

Injectivity of Power Function for Positive Non-Unit Elements: $a^m = a^n \leftrightarrow m = n$

Informal description

For any element $a > 0$ with $a \neq 1$ in a preorder with a multiplication operation, the equality $a^m = a^n$ holds if and only if $m = n$ for any natural numbers $m$ and $n$.

pow_le_one_iff_of_nonneg theorem

(ha : 0 ≤ a) (hn : n ≠ 0) : a ^ n ≤ 1 ↔ a ≤ 1

Full source

lemma pow_le_one_iff_of_nonneg (ha : 0 ≤ a) (hn : n ≠ 0) : a ^ n ≤ 1 ↔ a ≤ 1 := by
  refine ⟨fun h ↦ ?_, pow_le_one₀ ha⟩
  contrapose! h
  exact one_lt_pow₀ h hn

Power Inequality: $a^n \leq 1 \leftrightarrow a \leq 1$ for $a \geq 0$ and $n \neq 0$

Informal description

For any element $a$ in a preordered type with a multiplication operation, if $a$ is nonnegative ($0 \leq a$) and $n$ is a nonzero natural number, then the inequality $a^n \leq 1$ holds if and only if $a \leq 1$.

one_le_pow_iff_of_nonneg theorem

(ha : 0 ≤ a) (hn : n ≠ 0) : 1 ≤ a ^ n ↔ 1 ≤ a

Full source

lemma one_le_pow_iff_of_nonneg (ha : 0 ≤ a) (hn : n ≠ 0) : 1 ≤ a ^ n ↔ 1 ≤ a := by
  refine ⟨fun h ↦ ?_, fun h ↦ one_le_pow₀ h⟩
  contrapose! h
  exact pow_lt_one₀ ha h hn

Characterization of Powers Greater Than or Equal to One: $1 \leq a^n \leftrightarrow 1 \leq a$ for $a \geq 0$ and $n \neq 0$

Informal description

For any element $a$ in a preordered type with a multiplication operation, if $a \geq 0$ and $n$ is a nonzero natural number, then $1 \leq a^n$ if and only if $1 \leq a$.

pow_lt_one_iff_of_nonneg theorem

(ha : 0 ≤ a) (hn : n ≠ 0) : a ^ n < 1 ↔ a < 1

Full source

lemma pow_lt_one_iff_of_nonneg (ha : 0 ≤ a) (hn : n ≠ 0) : a ^ n < 1 ↔ a < 1 :=
  lt_iff_lt_of_le_iff_le (one_le_pow_iff_of_nonneg ha hn)

Power Inequality: $a^n < 1 \leftrightarrow a < 1$ for $a \geq 0$ and $n \neq 0$

Informal description

For any element $a$ in a preordered type with a multiplication operation, if $a \geq 0$ and $n$ is a nonzero natural number, then $a^n < 1$ if and only if $a < 1$.

one_lt_pow_iff_of_nonneg theorem

(ha : 0 ≤ a) (hn : n ≠ 0) : 1 < a ^ n ↔ 1 < a

Full source

lemma one_lt_pow_iff_of_nonneg (ha : 0 ≤ a) (hn : n ≠ 0) : 1 < a ^ n ↔ 1 < a := by
  simp only [← not_le, pow_le_one_iff_of_nonneg ha hn]

Characterization of Powers Greater Than One: $1 < a^n \leftrightarrow 1 < a$ for $a \geq 0$ and $n \neq 0$

Informal description

For any nonnegative element $a$ in a preordered type with a multiplication operation and any nonzero natural number $n$, the inequality $1 < a^n$ holds if and only if $1 < a$.

pow_eq_one_iff_of_nonneg theorem

(ha : 0 ≤ a) (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1

Full source

lemma pow_eq_one_iff_of_nonneg (ha : 0 ≤ a) (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 := by
  simp only [le_antisymm_iff, pow_le_one_iff_of_nonneg ha hn, one_le_pow_iff_of_nonneg ha hn]

Characterization of Powers Equal to One: $a^n = 1 \leftrightarrow a = 1$ for $a \geq 0$ and $n \neq 0$

Informal description

For any element $a$ in a preordered type with a multiplication operation, if $a$ is nonnegative ($0 \leq a$) and $n$ is a nonzero natural number, then $a^n = 1$ if and only if $a = 1$.

sq_le_one_iff₀ theorem

(ha : 0 ≤ a) : a ^ 2 ≤ 1 ↔ a ≤ 1

Full source

lemma sq_le_one_iff₀ (ha : 0 ≤ a) : a ^ 2 ≤ 1 ↔ a ≤ 1 :=
  pow_le_one_iff_of_nonneg ha (Nat.succ_ne_zero _)

Square Inequality for Nonnegative Elements: $a^2 \leq 1 \leftrightarrow a \leq 1$

Informal description

For any nonnegative element $a$ (i.e., $0 \leq a$), the inequality $a^2 \leq 1$ holds if and only if $a \leq 1$.

sq_lt_one_iff₀ theorem

(ha : 0 ≤ a) : a ^ 2 < 1 ↔ a < 1

Full source

lemma sq_lt_one_iff₀ (ha : 0 ≤ a) : a ^ 2 < 1 ↔ a < 1 :=
  pow_lt_one_iff_of_nonneg ha (Nat.succ_ne_zero _)

Square Inequality for Nonnegative Elements: $a^2 < 1 \leftrightarrow a < 1$

Informal description

For any nonnegative element $a$ (i.e., $0 \leq a$), the inequality $a^2 < 1$ holds if and only if $a < 1$.

one_le_sq_iff₀ theorem

(ha : 0 ≤ a) : 1 ≤ a ^ 2 ↔ 1 ≤ a

Full source

lemma one_le_sq_iff₀ (ha : 0 ≤ a) : 1 ≤ a ^ 2 ↔ 1 ≤ a :=
  one_le_pow_iff_of_nonneg ha (Nat.succ_ne_zero _)

Square of Nonnegative Element is Greater Than or Equal to One iff Element is Greater Than or Equal to One

Informal description

For any element $a$ in a preordered type with a multiplication operation, if $a \geq 0$, then $1 \leq a^2$ if and only if $1 \leq a$.

one_lt_sq_iff₀ theorem

(ha : 0 ≤ a) : 1 < a ^ 2 ↔ 1 < a

Full source

lemma one_lt_sq_iff₀ (ha : 0 ≤ a) : 1 < a ^ 2 ↔ 1 < a :=
  one_lt_pow_iff_of_nonneg ha (Nat.succ_ne_zero _)

Square of Nonnegative Element is Greater Than One iff Element is Greater Than One

Informal description

For any nonnegative element $a$ in a preordered type with a multiplication operation, the inequality $1 < a^2$ holds if and only if $1 < a$.

lt_of_pow_lt_pow_left₀ theorem

(n : ℕ) (hb : 0 ≤ b) (h : a ^ n < b ^ n) : a < b

Full source

lemma lt_of_pow_lt_pow_left₀ (n : ℕ) (hb : 0 ≤ b) (h : a ^ n < b ^ n) : a < b :=
  lt_of_not_ge fun hn => not_lt_of_ge (pow_le_pow_left₀ hb hn _) h

Strict Inequality Preservation Under Powers: $a^n < b^n$ implies $a < b$ for $b \geq 0$

Informal description

For any natural number $n$ and elements $a, b$ in a type with appropriate monotonicity properties, if $b \geq 0$ and $a^n < b^n$, then $a < b$.

le_of_pow_le_pow_left₀ theorem

(hn : n ≠ 0) (hb : 0 ≤ b) (h : a ^ n ≤ b ^ n) : a ≤ b

Full source

lemma le_of_pow_le_pow_left₀ (hn : n ≠ 0) (hb : 0 ≤ b) (h : a ^ n ≤ b ^ n) : a ≤ b :=
  le_of_not_lt fun h1 => not_le_of_lt (pow_lt_pow_left₀ h1 hb hn) h

Inequality Preservation Under Powers: $a^n \leq b^n$ implies $a \leq b$ for $b \geq 0$ and $n \neq 0$

Informal description

For any natural number $n \neq 0$ and elements $a, b$ in a type with appropriate monotonicity properties, if $b \geq 0$ and $a^n \leq b^n$, then $a \leq b$.

sq_eq_sq₀ theorem

(ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 = b ^ 2 ↔ a = b

Full source

@[simp]
lemma sq_eq_sq₀ (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 = b ^ 2 ↔ a = b :=
  pow_left_inj₀ ha hb (by decide)

Square Equality for Nonnegative Elements: $a^2 = b^2 \leftrightarrow a = b$ when $a, b \geq 0$

Informal description

For any nonnegative elements $a$ and $b$ in a preorder with a multiplication operation, the squares of $a$ and $b$ are equal if and only if $a$ and $b$ themselves are equal, i.e., $a^2 = b^2 \leftrightarrow a = b$.

lt_of_mul_self_lt_mul_self₀ theorem

(hb : 0 ≤ b) : a * a < b * b → a < b

Full source

lemma lt_of_mul_self_lt_mul_self₀ (hb : 0 ≤ b) : a * a < b * b → a < b := by
  simp only [← sq]
  exact lt_of_pow_lt_pow_left₀ _ hb

Strict Inequality Preservation Under Squaring: $a^2 < b^2$ implies $a < b$ for $b \geq 0$

Informal description

For any elements $a$ and $b$ in a type with appropriate monotonicity properties, if $b \geq 0$ and $a^2 < b^2$, then $a < b$.

sq_lt_sq₀ theorem

(ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 < b ^ 2 ↔ a < b

Full source

lemma sq_lt_sq₀ (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 < b ^ 2 ↔ a < b :=
  pow_lt_pow_iff_left₀ ha hb two_ne_zero

Square Inequality for Nonnegative Reals: $a^2 < b^2 \leftrightarrow a < b$ when $a, b \geq 0$

Informal description

For any nonnegative real numbers $a$ and $b$ (i.e., $a \geq 0$ and $b \geq 0$), the inequality $a^2 < b^2$ holds if and only if $a < b$.

sq_le_sq₀ theorem

(ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 ≤ b ^ 2 ↔ a ≤ b

Full source

lemma sq_le_sq₀ (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 ≤ b ^ 2 ↔ a ≤ b :=
  pow_le_pow_iff_left₀ ha hb two_ne_zero

Square Inequality for Nonnegative Reals: $a^2 \leq b^2 \leftrightarrow a \leq b$

Informal description

For any nonnegative real numbers $a$ and $b$ (i.e., $a \geq 0$ and $b \geq 0$), the inequality $a^2 \leq b^2$ holds if and only if $a \leq b$.

PosMulMono.toPosMulStrictMono theorem

[PosMulMono α] : PosMulStrictMono α

Full source

theorem PosMulMono.toPosMulStrictMono [PosMulMono α] : PosMulStrictMono α where
  elim := fun x _ _ h => (mul_le_mul_of_nonneg_left h.le x.2.le).lt_of_ne
    (h.ne ∘ mul_left_cancel₀ x.2.ne')

Implication from Monotonicity to Strict Monotonicity for Left Multiplication by Positive Elements

Informal description

If left multiplication by nonnegative elements is monotone in a preorder $\alpha$ (i.e., `PosMulMono α` holds), then left multiplication by positive elements is strictly monotone (i.e., `PosMulStrictMono α` holds).

posMulMono_iff_posMulStrictMono theorem

: PosMulMono α ↔ PosMulStrictMono α

Full source

theorem posMulMono_iff_posMulStrictMono : PosMulMonoPosMulMono α ↔ PosMulStrictMono α :=
  ⟨@PosMulMono.toPosMulStrictMono α _ _, @PosMulStrictMono.toPosMulMono α _ _⟩

Equivalence of Monotonicity and Strict Monotonicity for Left Multiplication

Informal description

For a preorder $\alpha$, left multiplication by nonnegative elements is monotone if and only if left multiplication by positive elements is strictly monotone. That is, the following are equivalent: 1. For all $b \geq 0$ and $a_1 \leq a_2$ in $\alpha$, we have $b \cdot a_1 \leq b \cdot a_2$. 2. For all $b > 0$ and $a_1 < a_2$ in $\alpha$, we have $b \cdot a_1 < b \cdot a_2$.

MulPosMono.toMulPosStrictMono theorem

[MulPosMono α] : MulPosStrictMono α

Full source

theorem MulPosMono.toMulPosStrictMono [MulPosMono α] : MulPosStrictMono α where
  elim := fun x _ _ h => (mul_le_mul_of_nonneg_right h.le x.2.le).lt_of_ne
    (h.ne ∘ mul_right_cancel₀ x.2.ne')

Implication from Monotonicity to Strict Monotonicity for Right Multiplication by Positive Elements

Informal description

If right multiplication by nonnegative elements is monotone in a preorder $\alpha$ (i.e., `MulPosMono α` holds), then right multiplication by positive elements is strictly monotone (i.e., `MulPosStrictMono α` holds).

mulPosMono_iff_mulPosStrictMono theorem

: MulPosMono α ↔ MulPosStrictMono α

Full source

theorem mulPosMono_iff_mulPosStrictMono : MulPosMonoMulPosMono α ↔ MulPosStrictMono α :=
  ⟨@MulPosMono.toMulPosStrictMono α _ _, @MulPosStrictMono.toMulPosMono α _ _⟩

Equivalence of Monotonicity and Strict Monotonicity for Right Multiplication in Preorders

Informal description

For a preorder $\alpha$, right multiplication by nonnegative elements is monotone if and only if right multiplication by positive elements is strictly monotone. That is, the following are equivalent: 1. For all $b \geq 0$ and $a_1 \leq a_2$, we have $a_1 \cdot b \leq a_2 \cdot b$. 2. For all $b > 0$ and $a_1 < a_2$, we have $a_1 \cdot b < a_2 \cdot b$.

PosMulReflectLT.toPosMulReflectLE theorem

[PosMulReflectLT α] : PosMulReflectLE α

Full source

theorem PosMulReflectLT.toPosMulReflectLE [PosMulReflectLT α] : PosMulReflectLE α where
  elim := fun x _ _ h =>
    h.eq_or_lt.elim (le_of_eqle_of_eq ∘ mul_left_cancel₀ x.2.ne.symm) fun h' =>
      (lt_of_mul_lt_mul_left h' x.2.le).le

Reflection of Non-Strict Order from Strict Order under Left Multiplication

Informal description

If left multiplication by nonnegative elements reflects the strict order in a preorder $\alpha$ (i.e., `PosMulReflectLT α` holds), then left multiplication by positive elements reflects the non-strict order (i.e., `PosMulReflectLE α` holds).

posMulReflectLE_iff_posMulReflectLT theorem

: PosMulReflectLE α ↔ PosMulReflectLT α

Full source

theorem posMulReflectLE_iff_posMulReflectLT : PosMulReflectLEPosMulReflectLE α ↔ PosMulReflectLT α :=
  ⟨@PosMulReflectLE.toPosMulReflectLT α _ _, @PosMulReflectLT.toPosMulReflectLE α _ _⟩

Equivalence of Order Reflection Properties for Left Multiplication

Informal description

For any preorder $\alpha$, the following are equivalent: 1. Left multiplication by positive elements reflects the non-strict order (i.e., $b \cdot a_1 \leq b \cdot a_2$ implies $a_1 \leq a_2$ for $b > 0$). 2. Left multiplication by nonnegative elements reflects the strict order (i.e., $b \cdot a_1 < b \cdot a_2$ implies $a_1 < a_2$ for $b \geq 0$).

MulPosReflectLT.toMulPosReflectLE theorem

[MulPosReflectLT α] : MulPosReflectLE α

Full source

theorem MulPosReflectLT.toMulPosReflectLE [MulPosReflectLT α] : MulPosReflectLE α where
  elim := fun x _ _ h => h.eq_or_lt.elim (le_of_eqle_of_eq ∘ mul_right_cancel₀ x.2.ne.symm) fun h' =>
    (lt_of_mul_lt_mul_right h' x.2.le).le

Reflection of Non-Strict Order from Strict Order under Right Multiplication

Informal description

If right multiplication by nonnegative elements reflects the strict order in a preorder $\alpha$ (i.e., `MulPosReflectLT α` holds), then right multiplication by positive elements reflects the non-strict order (i.e., `MulPosReflectLE α` holds).

mulPosReflectLE_iff_mulPosReflectLT theorem

: MulPosReflectLE α ↔ MulPosReflectLT α

Full source

theorem mulPosReflectLE_iff_mulPosReflectLT : MulPosReflectLEMulPosReflectLE α ↔ MulPosReflectLT α :=
  ⟨@MulPosReflectLE.toMulPosReflectLT α _ _, @MulPosReflectLT.toMulPosReflectLE α _ _⟩

Equivalence of Order Reflection Properties under Right Multiplication

Informal description

For any preorder $\alpha$, the following are equivalent: 1. Right multiplication by positive elements reflects the non-strict order (i.e., $a_1 * b \leq a_2 * b$ implies $a_1 \leq a_2$ for $b > 0$). 2. Right multiplication by nonnegative elements reflects the strict order (i.e., $a_1 * b < a_2 * b$ implies $a_1 < a_2$ for $b \geq 0$).

mul_inv_left_le theorem

(hb : 0 ≤ b) : a * (a⁻¹ * b) ≤ b

Full source

/-- Equality holds when `a ≠ 0`. See `mul_inv_cancel_left`. -/
lemma mul_inv_left_le (hb : 0 ≤ b) : a * (a⁻¹ * b) ≤ b := by
  obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

Left Multiplication by Inverse Preserves Nonnegativity: $a \cdot (a^{-1} \cdot b) \leq b$ for $b \geq 0$

Informal description

For any elements $a$ and $b$ in a division monoid $\alpha$, if $b$ is nonnegative (i.e., $0 \leq b$), then the inequality $a \cdot (a^{-1} \cdot b) \leq b$ holds.

le_mul_inv_left theorem

(hb : b ≤ 0) : b ≤ a * (a⁻¹ * b)

Full source

/-- Equality holds when `a ≠ 0`. See `mul_inv_cancel_left`. -/
lemma le_mul_inv_left (hb : b ≤ 0) : b ≤ a * (a⁻¹ * b) := by
  obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

Left Multiplication by Inverse Preserves Nonpositive Elements

Informal description

For any element $b$ in a division monoid $\alpha$ such that $b \leq 0$, it holds that $b \leq a \cdot (a^{-1} \cdot b)$.

inv_mul_left_le theorem

(hb : 0 ≤ b) : a⁻¹ * (a * b) ≤ b

Full source

/-- Equality holds when `a ≠ 0`. See `inv_mul_cancel_left`. -/
lemma inv_mul_left_le (hb : 0 ≤ b) : a⁻¹ * (a * b) ≤ b := by
  obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

Left inverse multiplication inequality in division monoids

Informal description

For any element $b$ in a division monoid $\alpha$ with $0 \leq b$, the inequality $a^{-1} \cdot (a \cdot b) \leq b$ holds.

le_inv_mul_left theorem

(hb : b ≤ 0) : b ≤ a⁻¹ * (a * b)

Full source

/-- Equality holds when `a ≠ 0`. See `inv_mul_cancel_left`. -/
lemma le_inv_mul_left (hb : b ≤ 0) : b ≤ a⁻¹ * (a * b) := by
  obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

Inequality for Negative Elements in Division Monoid: $b \leq a^{-1}(a b)$ when $b \leq 0$

Informal description

For any elements $a$ and $b$ in a division monoid, if $b \leq 0$, then $b \leq a^{-1} * (a * b)$.

mul_inv_right_le theorem

(ha : 0 ≤ a) : a * b * b⁻¹ ≤ a

Full source

/-- Equality holds when `b ≠ 0`. See `mul_inv_cancel_right`. -/
lemma mul_inv_right_le (ha : 0 ≤ a) : a * b * b⁻¹ ≤ a := by
  obtain rfl | hb := eq_or_ne b 0 <;> simp [*]

Right Multiplication by Inverse Preserves Order for Nonnegative Elements

Informal description

For any elements $a$ and $b$ in a division monoid, if $a$ is nonnegative ($0 \leq a$), then $a \cdot b \cdot b^{-1} \leq a$.

le_mul_inv_right theorem

(ha : a ≤ 0) : a ≤ a * b * b⁻¹

Full source

/-- Equality holds when `b ≠ 0`. See `mul_inv_cancel_right`. -/
lemma le_mul_inv_right (ha : a ≤ 0) : a ≤ a * b * b⁻¹ := by
  obtain rfl | hb := eq_or_ne b 0 <;> simp [*]

Lower bound for negative elements under right multiplication by inverse: $a \leq a \cdot b \cdot b^{-1}$ when $a \leq 0$

Informal description

For any elements $a$ and $b$ in a division monoid, if $a \leq 0$, then $a \leq a \cdot b \cdot b^{-1}$.

inv_mul_right_le theorem

(ha : 0 ≤ a) : a * b⁻¹ * b ≤ a

Full source

/-- Equality holds when `b ≠ 0`. See `inv_mul_cancel_right`. -/
lemma inv_mul_right_le (ha : 0 ≤ a) : a * b⁻¹ * b ≤ a := by
  obtain rfl | hb := eq_or_ne b 0 <;> simp [*]

Inequality for Right Inverse Multiplication: $a \cdot b^{-1} \cdot b \leq a$ when $0 \leq a$

Informal description

For any element $a$ in a division monoid with $0 \leq a$, and any element $b$, the inequality $a \cdot b^{-1} \cdot b \leq a$ holds.

le_inv_mul_right theorem

(ha : a ≤ 0) : a ≤ a * b⁻¹ * b

Full source

/-- Equality holds when `b ≠ 0`. See `inv_mul_cancel_right`. -/
lemma le_inv_mul_right (ha : a ≤ 0) : a ≤ a * b⁻¹ * b := by
  obtain rfl | hb := eq_or_ne b 0 <;> simp [*]

Inequality for Right Multiplication by Inverse: $a \leq a \cdot b^{-1} \cdot b$ when $a \leq 0$

Informal description

For any element $a$ in a group with zero such that $a \leq 0$, it holds that $a \leq a \cdot b^{-1} \cdot b$.

mul_div_mul_right_le theorem

(h : 0 ≤ a / b) : a * c / (b * c) ≤ a / b

Full source

/-- Equality holds when `c ≠ 0`. See `mul_div_mul_right`. -/
lemma mul_div_mul_right_le (h : 0 ≤ a / b) : a * c / (b * c) ≤ a / b := by
  obtain rfl | hc := eq_or_ne c 0
  · simpa
  · rw [mul_div_mul_right _ _ hc]

Inequality for Right Multiplication and Division: $(a \cdot c)/(b \cdot c) \leq a/b$ when $0 \leq a/b$

Informal description

For any elements $a$, $b$, and $c$ in a group with zero, if $0 \leq a / b$, then $(a \cdot c) / (b \cdot c) \leq a / b$.

le_mul_div_mul_right theorem

(h : a / b ≤ 0) : a / b ≤ a * c / (b * c)

Full source

/-- Equality holds when `c ≠ 0`. See `mul_div_mul_right`. -/
lemma le_mul_div_mul_right (h : a / b ≤ 0) : a / b ≤ a * c / (b * c) := by
  obtain rfl | hc := eq_or_ne c 0
  · simpa
  · rw [mul_div_mul_right _ _ hc]

Inequality for Right Multiplication in Division When Quotient is Non-positive

Informal description

For elements $a, b, c$ in a group with zero, if $a/b \leq 0$, then $a/b \leq (a \cdot c)/(b \cdot c)$.

div_self_le_one theorem

(a : G₀) : a / a ≤ 1

Full source

/-- See `div_self` for the version with equality when `a ≠ 0`. -/
lemma div_self_le_one (a : G₀) : a / a ≤ 1 := by obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

Quotient of Element with Itself is at Most One: $a/a \leq 1$

Informal description

For any element $a$ in a group with zero, the quotient of $a$ divided by itself is less than or equal to $1$, i.e., $a / a \leq 1$.

mul_inv_le_one theorem

: a * a⁻¹ ≤ 1

Full source

/-- Equality holds when `a ≠ 0`. See `mul_inv_cancel`. -/
lemma mul_inv_le_one : a * a⁻¹ ≤ 1 := by simpa only [div_eq_mul_inv] using div_self_le_one a

Product-Inverse Inequality: $a \cdot a^{-1} \leq 1$

Informal description

For any element $a$ in a division monoid, the product of $a$ and its inverse is less than or equal to $1$, i.e., $a \cdot a^{-1} \leq 1$.

inv_mul_le_one theorem

: a⁻¹ * a ≤ 1

Full source

/-- Equality holds when `a ≠ 0`. See `inv_mul_cancel`. -/
lemma inv_mul_le_one : a⁻¹ * a ≤ 1 := by obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

Inverse-Product Inequality: $a^{-1} \cdot a \leq 1$

Informal description

For any element $a$ in a division monoid, the product of its inverse and itself is less than or equal to the multiplicative identity, i.e., $a^{-1} \cdot a \leq 1$.

inv_pos theorem

: 0 < a⁻¹ ↔ 0 < a

Full source

@[simp] lemma inv_pos : 0 < a⁻¹ ↔ 0 < a := by
  suffices ∀ a : G₀, 0 < a → 0 < a⁻¹ from ⟨fun h ↦ inv_inv a ▸ this _ h, this a⟩
  intro a ha
  apply lt_of_mul_lt_mul_left _ ha.le
  apply lt_of_mul_lt_mul_left _ ha.le
  simpa [ha.ne']

Positivity of Inverse Equals Positivity of Element

Informal description

For any element $a$ in a division monoid, the inverse $a^{-1}$ is positive if and only if $a$ is positive, i.e., $0 < a^{-1} \leftrightarrow 0 < a$.

inv_nonneg theorem

: 0 ≤ a⁻¹ ↔ 0 ≤ a

Full source

@[simp] lemma inv_nonneg : 0 ≤ a⁻¹ ↔ 0 ≤ a := by simp only [le_iff_eq_or_lt, inv_pos, zero_eq_inv]

Nonnegativity of Inverse Equals Nonnegativity of Element

Informal description

For any element $a$ in a division monoid, the inequality $0 \leq a^{-1}$ holds if and only if $0 \leq a$.

one_div_pos theorem

: 0 < 1 / a ↔ 0 < a

Full source

lemma one_div_pos : 0 < 1 / a ↔ 0 < a := one_div a ▸ inv_pos

Positivity of Reciprocal Equals Positivity of Element

Informal description

For any element $a$ in a division monoid, the reciprocal $\frac{1}{a}$ is positive if and only if $a$ is positive, i.e., $0 < \frac{1}{a} \leftrightarrow 0 < a$.

one_div_nonneg theorem

: 0 ≤ 1 / a ↔ 0 ≤ a

Full source

lemma one_div_nonneg : 0 ≤ 1 / a ↔ 0 ≤ a := one_div a ▸ inv_nonneg

Nonnegativity of Reciprocal Equals Nonnegativity of Element

Informal description

For any element $a$ in a division monoid, the inequality $0 \leq \frac{1}{a}$ holds if and only if $0 \leq a$.

PosMulReflectLT.toPosMulStrictMono theorem

: PosMulStrictMono G₀

Full source

/-- For a group with zero, `PosMulReflectLT G₀` implies `PosMulStrictMono G₀`. -/
theorem PosMulReflectLT.toPosMulStrictMono : PosMulStrictMono G₀ where
  elim := by
    rintro ⟨a, ha⟩ b c hlt
    apply lt_of_mul_lt_mul_left _ (inv_pos_of_pos ha).le
    simpa [ha.ne']

Strict monotonicity of left multiplication by positive elements in a group with zero

Informal description

For a group with zero $G_0$, if left multiplication by nonnegative elements reflects the strict order (i.e., $G_0$ satisfies `PosMulReflectLT`), then left multiplication by positive elements is strictly monotone (i.e., $G_0$ satisfies `PosMulStrictMono`).

MulPosReflectLE.of_posMulReflectLT_of_mulPosMono theorem

[MulPosMono G₀] : MulPosReflectLE G₀

Full source

/-- For a group with zero, `PosMulReflectLT G₀`
allows us to upgrade `MulPosMono G₀` to `MulPosReflectLE G₀`.
The other implication holds without the `PosMulReflectLT G₀` assumption,
see `MulPosReflectLT.toMulPosStrictMono` for a stronger version below.

This theorem shows that in the presence of the assumption `PosMulReflectLT G₀`,
it makes no sense to optimize between assumptions `MulPosMono G₀`, `MulPosStrictMono G₀`,
`MulPosReflectLT G₀`, and `MulPosReflectLE G₀`. -/
theorem MulPosReflectLE.of_posMulReflectLT_of_mulPosMono [MulPosMono G₀] : MulPosReflectLE G₀ where
  elim := by
    rintro ⟨a, ha⟩ b c h
    simpa [ha.ne'] using mul_le_mul_of_nonneg_right h (inv_nonneg.2 ha.le)

Reflection of Non-Strict Order under Right Multiplication by Positive Elements via Monotonicity and Strict Order Reflection

Informal description

Let $G₀$ be a group with zero. If right multiplication by nonnegative elements is monotone (i.e., $G₀$ satisfies `MulPosMono`) and left multiplication by nonnegative elements reflects the strict order (i.e., $G₀$ satisfies `PosMulReflectLT`), then right multiplication by positive elements reflects the non-strict order (i.e., $G₀$ satisfies `MulPosReflectLE`).

div_pos theorem

(ha : 0 < a) (hb : 0 < b) : 0 < a / b

Full source

lemma div_pos (ha : 0 < a) (hb : 0 < b) : 0 < a / b := by
  rw [div_eq_mul_inv]; exact mul_pos ha (inv_pos.2 hb)

Positivity of Quotient for Positive Elements

Informal description

For any elements $a$ and $b$ in a division monoid, if $0 < a$ and $0 < b$, then $0 < a / b$.

div_nonneg theorem

(ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a / b

Full source

lemma div_nonneg (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a / b := by
  rw [div_eq_mul_inv]; exact mul_nonneg ha (inv_nonneg.2 hb)

Nonnegativity of Division: $0 \leq a / b$ under $0 \leq a$ and $0 \leq b$

Informal description

For any elements $a$ and $b$ in a division monoid, if $0 \leq a$ and $0 \leq b$, then $0 \leq a / b$.

le_inv_mul_iff₀ theorem

(hc : 0 < c) : a ≤ c⁻¹ * b ↔ c * a ≤ b

Full source

/-- See `le_inv_mul_iff₀'` for a version with multiplication on the other side. -/
lemma le_inv_mul_iff₀ (hc : 0 < c) : a ≤ c⁻¹ * b ↔ c * a ≤ b := by
  rw [← mul_le_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ hc.ne']

Inequality Equivalence under Left Multiplication by Inverse: $a \leq c^{-1} \cdot b \leftrightarrow c \cdot a \leq b$ for $c > 0$

Informal description

For any positive element $c$ in a group with zero, the inequality $a \leq c^{-1} \cdot b$ holds if and only if $c \cdot a \leq b$.

inv_mul_le_iff₀ theorem

(hc : 0 < c) : c⁻¹ * b ≤ a ↔ b ≤ c * a

Full source

/-- See `inv_mul_le_iff₀'` for a version with multiplication on the other side. -/
lemma inv_mul_le_iff₀ (hc : 0 < c) : c⁻¹c⁻¹ * b ≤ a ↔ b ≤ c * a := by
  rw [← mul_le_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ hc.ne']

Inverse Multiplication Inequality: $c^{-1}b \leq a \leftrightarrow b \leq ca$ for $c > 0$

Informal description

For any positive element $c$ in a group with zero, the inequality $c^{-1} \cdot b \leq a$ holds if and only if $b \leq c \cdot a$.

one_le_inv_mul₀ theorem

(ha : 0 < a) : 1 ≤ a⁻¹ * b ↔ a ≤ b

Full source

lemma one_le_inv_mul₀ (ha : 0 < a) : 1 ≤ a⁻¹ * b ↔ a ≤ b := by rw [le_inv_mul_iff₀ ha, mul_one]

Inequality Equivalence: $1 \leq a^{-1}b \leftrightarrow a \leq b$ for $a > 0$

Informal description

For any positive element $a$ in a group with zero, the inequality $1 \leq a^{-1} \cdot b$ holds if and only if $a \leq b$.

inv_mul_le_one₀ theorem

(ha : 0 < a) : a⁻¹ * b ≤ 1 ↔ b ≤ a

Full source

lemma inv_mul_le_one₀ (ha : 0 < a) : a⁻¹a⁻¹ * b ≤ 1 ↔ b ≤ a := by rw [inv_mul_le_iff₀ ha, mul_one]

Inverse Multiplication Inequality: $a^{-1}b \leq 1 \leftrightarrow b \leq a$ for $a > 0$

Informal description

For any positive element $a$ in a group with zero, the inequality $a^{-1} \cdot b \leq 1$ holds if and only if $b \leq a$.

inv_le_iff_one_le_mul₀' theorem

(ha : 0 < a) : a⁻¹ ≤ b ↔ 1 ≤ a * b

Full source

/-- See `inv_le_iff_one_le_mul₀` for a version with multiplication on the other side. -/
lemma inv_le_iff_one_le_mul₀' (ha : 0 < a) : a⁻¹a⁻¹ ≤ b ↔ 1 ≤ a * b := by
  rw [← inv_mul_le_iff₀ ha, mul_one]

Inverse Inequality: $a^{-1} \leq b \leftrightarrow 1 \leq a b$ for $a > 0$

Informal description

For any positive element $a$ in a group with zero, the inequality $a^{-1} \leq b$ holds if and only if $1 \leq a \cdot b$.

one_le_inv₀ theorem

(ha : 0 < a) : 1 ≤ a⁻¹ ↔ a ≤ 1

Full source

lemma one_le_inv₀ (ha : 0 < a) : 1 ≤ a⁻¹ ↔ a ≤ 1 := by simpa using one_le_inv_mul₀ ha (b := 1)

Inverse Inequality: $1 \leq a^{-1} \leftrightarrow a \leq 1$ for $a > 0$

Informal description

For any positive element $a$ in a group with zero, the inequality $1 \leq a^{-1}$ holds if and only if $a \leq 1$.

inv_le_one₀ theorem

(ha : 0 < a) : a⁻¹ ≤ 1 ↔ 1 ≤ a

Full source

lemma inv_le_one₀ (ha : 0 < a) : a⁻¹a⁻¹ ≤ 1 ↔ 1 ≤ a := by simpa using inv_mul_le_one₀ ha (b := 1)

Inverse Inequality: $a^{-1} \leq 1 \leftrightarrow 1 \leq a$ for $a > 0$

Informal description

For any positive element $a$ in a group with zero, the inequality $a^{-1} \leq 1$ holds if and only if $1 \leq a$.

mul_le_of_le_inv_mul₀ theorem

(hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ c⁻¹ * b) : c * a ≤ b

Full source

/-- One direction of `le_inv_mul_iff₀` where `c` is allowed to be `0` (but `b` must be nonnegative).
-/
lemma mul_le_of_le_inv_mul₀ (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ c⁻¹ * b) : c * a ≤ b := by
  obtain rfl | hc := hc.eq_or_lt
  · simpa using hb
  · rwa [le_inv_mul_iff₀ hc] at h

Inequality Preservation under Left Multiplication: $a \leq c^{-1} \cdot b \Rightarrow c \cdot a \leq b$ for $b, c \geq 0$

Informal description

For any nonnegative elements $b$ and $c$ in a group with zero, if $a \leq c^{-1} \cdot b$, then $c \cdot a \leq b$.

inv_mul_le_of_le_mul₀ theorem

(hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ b * c) : b⁻¹ * a ≤ c

Full source

/-- One direction of `inv_mul_le_iff₀` where `b` is allowed to be `0` (but `c` must be nonnegative).
-/
lemma inv_mul_le_of_le_mul₀ (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ b * c) : b⁻¹ * a ≤ c := by
  obtain rfl | hb := hb.eq_or_lt
  · simp [hc]
  · rwa [inv_mul_le_iff₀ hb]

Inverse Multiplication Inequality: $a \leq b \cdot c \Rightarrow b^{-1} \cdot a \leq c$ for $b, c \geq 0$

Informal description

For any nonnegative elements $b$ and $c$ in a group with zero, if $a \leq b \cdot c$, then $b^{-1} \cdot a \leq c$.

lt_inv_mul_iff₀ theorem

(hc : 0 < c) : a < c⁻¹ * b ↔ c * a < b

Full source

/-- See `lt_inv_mul_iff₀'` for a version with multiplication on the other side. -/
lemma lt_inv_mul_iff₀ (hc : 0 < c) : a < c⁻¹ * b ↔ c * a < b := by
  rw [← mul_lt_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ hc.ne']

Inequality Equivalence under Left Multiplication by Inverse in Group with Zero

Informal description

For any positive element $c$ in a group with zero, the inequality $a < c^{-1} \cdot b$ holds if and only if $c \cdot a < b$.

inv_mul_lt_iff₀ theorem

(hc : 0 < c) : c⁻¹ * b < a ↔ b < c * a

Full source

/-- See `inv_mul_lt_iff₀'` for a version with multiplication on the other side. -/
lemma inv_mul_lt_iff₀ (hc : 0 < c) : c⁻¹c⁻¹ * b < a ↔ b < c * a := by
  rw [← mul_lt_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ hc.ne']

Inverse Multiplication Inequality: $c^{-1}b < a \leftrightarrow b < ca$ for $c > 0$

Informal description

For any positive element $c$ in a group with zero, the inequality $c^{-1} \cdot b < a$ holds if and only if $b < c \cdot a$.

inv_lt_iff_one_lt_mul₀' theorem

(ha : 0 < a) : a⁻¹ < b ↔ 1 < a * b

Full source

/-- See `inv_lt_iff_one_lt_mul₀` for a version with multiplication on the other side. -/
lemma inv_lt_iff_one_lt_mul₀' (ha : 0 < a) : a⁻¹a⁻¹ < b ↔ 1 < a * b := by
  rw [← inv_mul_lt_iff₀ ha, mul_one]

Inverse Inequality Equivalence: $a^{-1} 0$

Informal description

For any positive element $a$ in a group with zero, the inequality $a^{-1} < b$ holds if and only if $1 < a \cdot b$.

one_lt_inv_mul₀ theorem

(ha : 0 < a) : 1 < a⁻¹ * b ↔ a < b

Full source

lemma one_lt_inv_mul₀ (ha : 0 < a) : 1 < a⁻¹ * b ↔ a < b := by rw [lt_inv_mul_iff₀ ha, mul_one]

Inequality Equivalence: $1 < a^{-1}b \leftrightarrow a < b$ for $a > 0$

Informal description

For any positive element $a$ in a group with zero, the inequality $1 < a^{-1} \cdot b$ holds if and only if $a < b$.

inv_mul_lt_one₀ theorem

(ha : 0 < a) : a⁻¹ * b < 1 ↔ b < a

Full source

lemma inv_mul_lt_one₀ (ha : 0 < a) : a⁻¹a⁻¹ * b < 1 ↔ b < a := by rw [inv_mul_lt_iff₀ ha, mul_one]

Inverse Multiplication Inequality: $a^{-1}b < 1 \leftrightarrow b < a$ for $a > 0$

Informal description

For any positive element $a$ in a group with zero, the inequality $a^{-1} \cdot b < 1$ holds if and only if $b < a$.

one_lt_inv₀ theorem

(ha : 0 < a) : 1 < a⁻¹ ↔ a < 1

Full source

lemma one_lt_inv₀ (ha : 0 < a) : 1 < a⁻¹ ↔ a < 1 := by simpa using one_lt_inv_mul₀ ha (b := 1)

Inverse Inequality: $1 < a^{-1} \leftrightarrow a < 1$ for $a > 0$

Informal description

For any positive element $a$ in a group with zero, the inequality $1 < a^{-1}$ holds if and only if $a < 1$.

inv_lt_one₀ theorem

(ha : 0 < a) : a⁻¹ < 1 ↔ 1 < a

Full source

lemma inv_lt_one₀ (ha : 0 < a) : a⁻¹a⁻¹ < 1 ↔ 1 < a := by simpa using inv_mul_lt_one₀ ha (b := 1)

Inverse Inequality: $a^{-1} < 1 \leftrightarrow 1 < a$ for $a > 0$

Informal description

For any positive element $a$ in a group with zero, the inverse of $a$ is less than $1$ if and only if $1 < a$, i.e., $a^{-1} < 1 \leftrightarrow 1 < a$.

inv_lt_one_of_one_lt₀ theorem

(ha : 1 < a) : a⁻¹ < 1

Full source

@[bound]
lemma inv_lt_one_of_one_lt₀ (ha : 1 < a) : a⁻¹ < 1 := (inv_lt_one₀ <| zero_lt_one.trans ha).2 ha

Inverse of Greater-Than-One Element is Less Than One

Informal description

For any element $a$ in a group with zero, if $1 < a$, then the inverse of $a$ is less than $1$, i.e., $a^{-1} < 1$.

one_lt_inv_iff₀ theorem

: 1 < a⁻¹ ↔ 0 < a ∧ a < 1

Full source

lemma one_lt_inv_iff₀ : 1 < a⁻¹ ↔ 0 < a ∧ a < 1 where
  mp h := ⟨inv_pos.1 (zero_lt_one.trans h), inv_inv a ▸ (inv_lt_one₀ <| zero_lt_one.trans h).2 h⟩
  mpr h := (one_lt_inv₀ h.1).2 h.2

Inverse Inequality: $1 < a^{-1} \leftrightarrow (0 < a \land a < 1)$

Informal description

For any element $a$ in a group with zero, the inequality $1 < a^{-1}$ holds if and only if $0 < a$ and $a < 1$.

inv_le_one_of_one_le₀ theorem

(ha : 1 ≤ a) : a⁻¹ ≤ 1

Full source

@[bound]
lemma inv_le_one_of_one_le₀ (ha : 1 ≤ a) : a⁻¹ ≤ 1 :=
  (inv_le_one₀ <| zero_lt_one.trans_le ha).2 ha

Inverse of Greater-Than-or-Equal-to-One Element is Less Than or Equal to One

Informal description

For any element $a$ in a group with zero, if $1 \leq a$, then the inverse of $a$ satisfies $a^{-1} \leq 1$.

one_le_inv_iff₀ theorem

: 1 ≤ a⁻¹ ↔ 0 < a ∧ a ≤ 1

Full source

lemma one_le_inv_iff₀ : 1 ≤ a⁻¹ ↔ 0 < a ∧ a ≤ 1 where
  mp h := ⟨inv_pos.1 (zero_lt_one.trans_le h),
    inv_inv a ▸ (inv_le_one₀ <| zero_lt_one.trans_le h).2 h⟩
  mpr h := (one_le_inv₀ h.1).2 h.2

Inverse Inequality: $1 \leq a^{-1} \leftrightarrow (0 < a \land a \leq 1)$

Informal description

For any element $a$ in a group with zero, the inequality $1 \leq a^{-1}$ holds if and only if $0 < a$ and $a \leq 1$.

inv_mul_le_one_of_le₀ theorem

(h : a ≤ b) (hb : 0 ≤ b) : b⁻¹ * a ≤ 1

Full source

@[bound]
lemma inv_mul_le_one_of_le₀ (h : a ≤ b) (hb : 0 ≤ b) : b⁻¹ * a ≤ 1 :=
  inv_mul_le_of_le_mul₀ hb zero_le_one <| by rwa [mul_one]

Inverse Multiplication Inequality: $a \leq b \implies b^{-1} \cdot a \leq 1$ for $b \geq 0$

Informal description

For any elements $a$ and $b$ in a division monoid with $b \geq 0$, if $a \leq b$, then $b^{-1} \cdot a \leq 1$.

zpow_nonneg theorem

(ha : 0 ≤ a) : ∀ n : ℤ, 0 ≤ a ^ n

Full source

lemma zpow_nonneg (ha : 0 ≤ a) : ∀ n : ℤ, 0 ≤ a ^ n
  | (n : ℕ) => by rw [zpow_natCast]; exact pow_nonneg ha _
  |-(n + 1 : ℕ) => by rw [zpow_neg, inv_nonneg, zpow_natCast]; exact pow_nonneg ha _

Nonnegativity of Integer Powers of Nonnegative Elements

Informal description

For any element $a$ in a division monoid with $a \geq 0$, and for any integer $n$, the $n$-th power of $a$ is nonnegative, i.e., $a^n \geq 0$.

zpow_pos theorem

(ha : 0 < a) : ∀ n : ℤ, 0 < a ^ n

Full source

lemma zpow_pos (ha : 0 < a) : ∀ n : ℤ, 0 < a ^ n
  | (n : ℕ) => by rw [zpow_natCast]; exact pow_pos ha _
  |-(n + 1 : ℕ) => by rw [zpow_neg, inv_pos, zpow_natCast]; exact pow_pos ha _

Positivity of Integer Powers: $a > 0 \implies a^n > 0$ for all $n \in \mathbb{Z}$

Informal description

For any positive element $a > 0$ in a division monoid and for any integer $n$, the $n$-th power of $a$ is positive, i.e., $a^n > 0$.

zpow_right_mono₀ theorem

(ha : 1 ≤ a) : Monotone fun n : ℤ ↦ a ^ n

Full source

lemma zpow_right_mono₀ (ha : 1 ≤ a) : Monotone fun n : ℤ ↦ a ^ n := by
  refine monotone_int_of_le_succ fun n ↦ ?_
  rw [zpow_add_one₀ (zero_lt_one.trans_le ha).ne']
  exact le_mul_of_one_le_right (zpow_nonneg (zero_le_one.trans ha) _) ha

Monotonicity of Integer Powers for Elements Greater Than or Equal to One

Informal description

Let $\alpha$ be a division monoid with a preorder structure. For any element $a \geq 1$, the function $n \mapsto a^n$ is monotone with respect to the integer parameter $n$.

zpow_right_anti₀ theorem

(ha₀ : 0 < a) (ha₁ : a ≤ 1) : Antitone fun n : ℤ ↦ a ^ n

Full source

lemma zpow_right_anti₀ (ha₀ : 0 < a) (ha₁ : a ≤ 1) : Antitone fun n : ℤ ↦ a ^ n := by
  refine antitone_int_of_succ_le fun n ↦ ?_
  rw [zpow_add_one₀ ha₀.ne']
  exact mul_le_of_le_one_right (zpow_nonneg ha₀.le _) ha₁

Antitonicity of Integer Powers for $0 < a \leq 1$

Informal description

For any element $a$ in a division monoid with $0 < a \leq 1$, the function $n \mapsto a^n$ is antitone (i.e., decreasing) with respect to the integer exponent $n$.

zpow_right_strictMono₀ theorem

(ha : 1 < a) : StrictMono fun n : ℤ ↦ a ^ n

Full source

lemma zpow_right_strictMono₀ (ha : 1 < a) : StrictMono fun n : ℤ ↦ a ^ n := by
  refine strictMono_int_of_lt_succ fun n ↦ ?_
  rw [zpow_add_one₀ (zero_lt_one.trans ha).ne']
  exact lt_mul_of_one_lt_right (zpow_pos (zero_lt_one.trans ha) _) ha

Strict Monotonicity of Integer Powers for $a > 1$

Informal description

For any element $a > 1$ in a division monoid, the integer power function $n \mapsto a^n$ is strictly increasing.

zpow_right_strictAnti₀ theorem

(ha₀ : 0 < a) (ha₁ : a < 1) : StrictAnti fun n : ℤ ↦ a ^ n

Full source

lemma zpow_right_strictAnti₀ (ha₀ : 0 < a) (ha₁ : a < 1) : StrictAnti fun n : ℤ ↦ a ^ n := by
  refine strictAnti_int_of_succ_lt fun n ↦ ?_
  rw [zpow_add_one₀ ha₀.ne']
  exact mul_lt_of_lt_one_right (zpow_pos ha₀ _) ha₁

Strict Antitonicity of Integer Powers for $0 < a < 1$

Informal description

For any element $a$ in a division monoid with $0 < a < 1$, the function $n \mapsto a^n$ is strictly antitone (i.e., strictly decreasing) with respect to the integer exponent $n$.

zpow_le_zpow_right₀ theorem

(ha : 1 ≤ a) (hmn : m ≤ n) : a ^ m ≤ a ^ n

Full source

@[gcongr]
lemma zpow_le_zpow_right₀ (ha : 1 ≤ a) (hmn : m ≤ n) : a ^ m ≤ a ^ n := zpow_right_mono₀ ha hmn

Monotonicity of integer powers for $a \geq 1$

Informal description

For any element $a \geq 1$ in a division monoid and integers $m \leq n$, the inequality $a^m \leq a^n$ holds.

zpow_le_zpow_right_of_le_one₀ theorem

(ha₀ : 0 < a) (ha₁ : a ≤ 1) (hmn : m ≤ n) : a ^ n ≤ a ^ m

Full source

@[gcongr]
lemma zpow_le_zpow_right_of_le_one₀ (ha₀ : 0 < a) (ha₁ : a ≤ 1) (hmn : m ≤ n) : a ^ n ≤ a ^ m :=
  zpow_right_anti₀ ha₀ ha₁ hmn

Monotonicity of Integer Powers for $0 < a \leq 1$: $a^n \leq a^m$ when $m \leq n$

Informal description

For any element $a$ in a division monoid with $0 < a \leq 1$ and integers $m \leq n$, the power $a^n$ is less than or equal to $a^m$, i.e., $a^n \leq a^m$.

one_le_zpow₀ theorem

(ha : 1 ≤ a) (hn : 0 ≤ n) : 1 ≤ a ^ n

Full source

lemma one_le_zpow₀ (ha : 1 ≤ a) (hn : 0 ≤ n) : 1 ≤ a ^ n := by simpa using zpow_right_mono₀ ha hn

Nonnegative Integer Power of Element Greater Than or Equal to One is At Least One

Informal description

For any element $a$ in a division monoid with a preorder structure, if $1 \leq a$ and $0 \leq n$ (where $n$ is an integer), then $1 \leq a^n$.

zpow_le_one₀ theorem

(ha₀ : 0 < a) (ha₁ : a ≤ 1) (hn : 0 ≤ n) : a ^ n ≤ 1

Full source

lemma zpow_le_one₀ (ha₀ : 0 < a) (ha₁ : a ≤ 1) (hn : 0 ≤ n) : a ^ n ≤ 1 := by
  simpa using zpow_right_anti₀ ha₀ ha₁ hn

Non-negative powers of elements between 0 and 1 are bounded by 1

Informal description

For any element $a$ in a division monoid with $0 < a \leq 1$ and any non-negative integer exponent $n$, the power $a^n$ satisfies $a^n \leq 1$.

zpow_le_one_of_nonpos₀ theorem

(ha : 1 ≤ a) (hn : n ≤ 0) : a ^ n ≤ 1

Full source

lemma zpow_le_one_of_nonpos₀ (ha : 1 ≤ a) (hn : n ≤ 0) : a ^ n ≤ 1 := by
  simpa using zpow_right_mono₀ ha hn

Nonpositive Integer Powers of Elements Greater Than or Equal to One Are At Most One

Informal description

For any element $a \geq 1$ in a division monoid $\alpha$ and any integer $n \leq 0$, the $n$-th power of $a$ satisfies $a^n \leq 1$.

one_le_zpow_of_nonpos₀ theorem

(ha₀ : 0 < a) (ha₁ : a ≤ 1) (hn : n ≤ 0) : 1 ≤ a ^ n

Full source

lemma one_le_zpow_of_nonpos₀ (ha₀ : 0 < a) (ha₁ : a ≤ 1) (hn : n ≤ 0) : 1 ≤ a ^ n := by
  simpa using zpow_right_anti₀ ha₀ ha₁ hn

$1 \leq a^n$ for $0 < a \leq 1$ and $n \leq 0$

Informal description

For any element $a$ in a division monoid with $0 < a \leq 1$ and any integer $n \leq 0$, we have $1 \leq a^n$.

zpow_lt_zpow_right₀ theorem

(ha : 1 < a) (hmn : m < n) : a ^ m < a ^ n

Full source

@[gcongr]
lemma zpow_lt_zpow_right₀ (ha : 1 < a) (hmn : m < n) : a ^ m < a ^ n :=
  zpow_right_strictMono₀ ha hmn

Strict Monotonicity of Integer Powers for $a > 1$: $m < n \Rightarrow a^m < a^n$

Informal description

For any element $a > 1$ in a division monoid and integers $m, n$, if $m < n$ then $a^m < a^n$.

zpow_lt_zpow_right_of_lt_one₀ theorem

(ha₀ : 0 < a) (ha₁ : a < 1) (hmn : m < n) : a ^ n < a ^ m

Full source

@[gcongr]
lemma zpow_lt_zpow_right_of_lt_one₀ (ha₀ : 0 < a) (ha₁ : a < 1) (hmn : m < n) : a ^ n < a ^ m :=
  zpow_right_strictAnti₀ ha₀ ha₁ hmn

Strict Antitonicity of Integer Powers for $0 < a < 1$

Informal description

For any element $a$ in a division monoid with $0 < a < 1$, and for any integers $m$ and $n$ such that $m < n$, the power $a^n$ is strictly less than $a^m$.

one_lt_zpow₀ theorem

(ha : 1 < a) (hn : 0 < n) : 1 < a ^ n

Full source

lemma one_lt_zpow₀ (ha : 1 < a) (hn : 0 < n) : 1 < a ^ n := by
  simpa using zpow_right_strictMono₀ ha hn

Positive Integer Powers of $a > 1$ Exceed One ($1 < a^n$)

Informal description

For any element $a > 1$ in a division monoid and any positive integer $n$, the $n$-th power of $a$ is greater than $1$, i.e., $1 < a^n$.

zpow_lt_one₀ theorem

(ha₀ : 0 < a) (ha₁ : a < 1) (hn : 0 < n) : a ^ n < 1

Full source

lemma zpow_lt_one₀ (ha₀ : 0 < a) (ha₁ : a < 1) (hn : 0 < n) : a ^ n < 1 := by
  simpa using zpow_right_strictAnti₀ ha₀ ha₁ hn

Positive integer powers of $0 < a < 1$ are less than one: $a^n < 1$ for $n > 0$

Informal description

For any element $a$ in a division monoid with $0 < a < 1$ and any positive integer $n$, the $n$-th power of $a$ is strictly less than $1$, i.e., $a^n < 1$.

zpow_lt_one_of_neg₀ theorem

(ha : 1 < a) (hn : n < 0) : a ^ n < 1

Full source

lemma zpow_lt_one_of_neg₀ (ha : 1 < a) (hn : n < 0) : a ^ n < 1 := by
  simpa using zpow_right_strictMono₀ ha hn

Negative Power of $a > 1$ is Less Than One: $a^n < 1$ for $n < 0$

Informal description

For any element $a > 1$ in a division monoid and any negative integer $n < 0$, the power $a^n$ is strictly less than $1$.

one_lt_zpow_of_neg₀ theorem

(ha₀ : 0 < a) (ha₁ : a < 1) (hn : n < 0) : 1 < a ^ n

Full source

lemma one_lt_zpow_of_neg₀ (ha₀ : 0 < a) (ha₁ : a < 1) (hn : n < 0) : 1 < a ^ n := by
  simpa using zpow_right_strictAnti₀ ha₀ ha₁ hn

Lower bound for negative powers of elements between 0 and 1: $1 < a^n$ when $0 < a < 1$ and $n < 0$

Informal description

For any element $a$ in a division monoid with $0 < a < 1$ and any negative integer $n$, the $n$-th power of $a$ satisfies $1 < a^n$.

zpow_le_zpow_iff_right₀ theorem

(ha : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n

Full source

@[simp] lemma zpow_le_zpow_iff_right₀ (ha : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n :=
  (zpow_right_strictMono₀ ha).le_iff_le

Comparison of Integer Powers for $a > 1$: $a^m \leq a^n \leftrightarrow m \leq n$

Informal description

For any element $a > 1$ in a division monoid, the inequality $a^m \leq a^n$ holds if and only if $m \leq n$.

zpow_lt_zpow_iff_right₀ theorem

(ha : 1 < a) : a ^ m < a ^ n ↔ m < n

Full source

@[simp] lemma zpow_lt_zpow_iff_right₀ (ha : 1 < a) : a ^ m < a ^ n ↔ m < n :=
  (zpow_right_strictMono₀ ha).lt_iff_lt

Strict Monotonicity of Integer Powers: $a^m < a^n \leftrightarrow m < n$ for $a > 1$

Informal description

For any element $a > 1$ in a division monoid, the inequality $a^m < a^n$ holds if and only if $m < n$, where $m$ and $n$ are integers.

zpow_le_zpow_iff_right_of_lt_one₀ theorem

(ha₀ : 0 < a) (ha₁ : a < 1) : a ^ m ≤ a ^ n ↔ n ≤ m

Full source

lemma zpow_le_zpow_iff_right_of_lt_one₀ (ha₀ : 0 < a) (ha₁ : a < 1) :
    a ^ m ≤ a ^ n ↔ n ≤ m := (zpow_right_strictAnti₀ ha₀ ha₁).le_iff_le

Inequality of Integer Powers for $0 < a < 1$: $a^m \leq a^n \leftrightarrow n \leq m$

Informal description

For any element $a$ in a division monoid with $0 < a < 1$, the inequality $a^m \leq a^n$ holds if and only if $n \leq m$.

zpow_lt_zpow_iff_right_of_lt_one₀ theorem

(ha₀ : 0 < a) (ha₁ : a < 1) : a ^ m < a ^ n ↔ n < m

Full source

lemma zpow_lt_zpow_iff_right_of_lt_one₀ (ha₀ : 0 < a) (ha₁ : a < 1) :
    a ^ m < a ^ n ↔ n < m := (zpow_right_strictAnti₀ ha₀ ha₁).lt_iff_lt

Strict Inequality of Integer Powers for $0 < a < 1$: $a^m < a^n \leftrightarrow n < m$

Informal description

For any element $a$ in a division monoid with $0 < a < 1$, and for any integers $m$ and $n$, the inequality $a^m < a^n$ holds if and only if $n < m$.

one_le_zpow_iff_right₀ theorem

(ha : 1 < a) : 1 ≤ a ^ n ↔ 0 ≤ n

Full source

@[simp] lemma one_le_zpow_iff_right₀ (ha : 1 < a) : 1 ≤ a ^ n ↔ 0 ≤ n := by
  simp [← zpow_le_zpow_iff_right₀ ha]

Comparison of Unit and Integer Power for $a > 1$: $1 \leq a^n \leftrightarrow 0 \leq n$

Informal description

For any element $a > 1$ in a division monoid and any integer $n$, the inequality $1 \leq a^n$ holds if and only if $0 \leq n$.

one_lt_zpow_iff_right₀ theorem

(ha : 1 < a) : 1 < a ^ n ↔ 0 < n

Full source

@[simp] lemma one_lt_zpow_iff_right₀ (ha : 1 < a) : 1 < a ^ n ↔ 0 < n := by
  simp [← zpow_lt_zpow_iff_right₀ ha]

Characterization of $1 < a^n$ for $a > 1$: $1 < a^n \leftrightarrow n > 0$

Informal description

For any element $a > 1$ in a division monoid, the inequality $1 < a^n$ holds if and only if $n > 0$, where $n$ is an integer.

one_le_zpow_iff_right_of_lt_one₀ theorem

(ha₀ : 0 < a) (ha₁ : a < 1) : 1 ≤ a ^ n ↔ n ≤ 0

Full source

@[simp] lemma one_le_zpow_iff_right_of_lt_one₀ (ha₀ : 0 < a) (ha₁ : a < 1) : 1 ≤ a ^ n ↔ n ≤ 0 := by
  simp [← zpow_le_zpow_iff_right_of_lt_one₀ ha₀ ha₁]

Inequality of One and Powers for $0 < a < 1$: $1 \leq a^n \leftrightarrow n \leq 0$

Informal description

For any element $a$ in a division monoid with $0 < a < 1$, the inequality $1 \leq a^n$ holds if and only if $n \leq 0$.

one_lt_zpow_iff_right_of_lt_one₀ theorem

(ha₀ : 0 < a) (ha₁ : a < 1) : 1 < a ^ n ↔ n < 0

Full source

@[simp] lemma one_lt_zpow_iff_right_of_lt_one₀ (ha₀ : 0 < a) (ha₁ : a < 1) : 1 < a ^ n ↔ n < 0 := by
  simp [← zpow_lt_zpow_iff_right_of_lt_one₀ ha₀ ha₁]

Inequality for Powers of $0 < a < 1$: $1 < a^n \leftrightarrow n < 0$

Informal description

For an element $a$ in a division monoid with $0 < a < 1$ and any integer $n$, we have $1 < a^n$ if and only if $n < 0$.

zpow_le_one_iff_right₀ theorem

(ha : 1 < a) : a ^ n ≤ 1 ↔ n ≤ 0

Full source

@[simp] lemma zpow_le_one_iff_right₀ (ha : 1 < a) : a ^ n ≤ 1 ↔ n ≤ 0 := by
  simp [← zpow_le_zpow_iff_right₀ ha]

Power Inequality for $a > 1$: $a^n \leq 1 \leftrightarrow n \leq 0$

Informal description

For any element $a > 1$ in a division monoid, the inequality $a^n \leq 1$ holds if and only if $n \leq 0$.

zpow_lt_one_iff_right₀ theorem

(ha : 1 < a) : a ^ n < 1 ↔ n < 0

Full source

@[simp] lemma zpow_lt_one_iff_right₀ (ha : 1 < a) : a ^ n < 1 ↔ n < 0 := by
  simp [← zpow_lt_zpow_iff_right₀ ha]

Negative Exponent Criterion for $a^n < 1$ when $a > 1$

Informal description

For any element $a > 1$ in a division monoid, the inequality $a^n < 1$ holds if and only if the integer exponent $n$ is negative, i.e., $n < 0$.

zpow_le_one_iff_right_of_lt_one₀ theorem

(ha₀ : 0 < a) (ha₁ : a < 1) : a ^ n ≤ 1 ↔ 0 ≤ n

Full source

@[simp] lemma zpow_le_one_iff_right_of_lt_one₀ (ha₀ : 0 < a) (ha₁ : a < 1) : a ^ n ≤ 1 ↔ 0 ≤ n := by
  simp [← zpow_le_zpow_iff_right_of_lt_one₀ ha₀ ha₁]

Inequality of Integer Powers for $0 < a < 1$: $a^n \leq 1 \leftrightarrow n \geq 0$

Informal description

For any element $a$ in a division monoid with $0 < a < 1$, the inequality $a^n \leq 1$ holds if and only if $n \geq 0$.

zpow_lt_one_iff_right_of_lt_one₀ theorem

(ha₀ : 0 < a) (ha₁ : a < 1) : a ^ n < 1 ↔ 0 < n

Full source

@[simp] lemma zpow_lt_one_iff_right_of_lt_one₀ (ha₀ : 0 < a) (ha₁ : a < 1) : a ^ n < 1 ↔ 0 < n := by
  simp [← zpow_lt_zpow_iff_right_of_lt_one₀ ha₀ ha₁]

Inequality for Integer Powers of $0 < a < 1$: $a^n < 1 \leftrightarrow n > 0$

Informal description

For any element $a$ in a division monoid with $0 < a < 1$ and any integer $n$, the inequality $a^n < 1$ holds if and only if $n$ is positive, i.e., $0 < n$.

Right.inv_pos theorem

: 0 < a⁻¹ ↔ 0 < a

Full source

lemma inv_pos : 0 < a⁻¹ ↔ 0 < a := by
  suffices ∀ a : G₀, 0 < a → 0 < a⁻¹ from ⟨fun h ↦ inv_inv a ▸ this _ h, this a⟩
  intro a ha
  apply lt_of_mul_lt_mul_right _ ha.le
  apply lt_of_mul_lt_mul_right _ ha.le
  simpa [ha.ne']

Positivity of Inverse in Division Monoid

Informal description

For any element $a$ in a division monoid, the inverse $a^{-1}$ is positive if and only if $a$ itself is positive, i.e., $0 < a^{-1} \leftrightarrow 0 < a$.

MulPosReflectLT.toMulPosStrictMono theorem

: MulPosStrictMono G₀

Full source

/-- For a group with zero, `MulPosReflectLT G₀` implies `MulPosStrictMono G₀`. -/
theorem _root_.MulPosReflectLT.toMulPosStrictMono : MulPosStrictMono G₀ where
  elim := by
    rintro ⟨a, ha⟩ b c hlt
    apply lt_of_mul_lt_mul_right _ (inv_pos.2 ha).le
    simpa [ha.ne']

Implication from Order Reflection to Strict Monotonicity under Right Multiplication in Groups with Zero

Informal description

For a group with zero $G_0$, if right multiplication by nonnegative elements reflects the strict order (i.e., the typeclass `MulPosReflectLT G₀` holds), then right multiplication by positive elements is strictly monotone (i.e., the typeclass `MulPosStrictMono G₀` holds).

Right.inv_nonneg theorem

: 0 ≤ a⁻¹ ↔ 0 ≤ a

Full source

lemma inv_nonneg : 0 ≤ a⁻¹ ↔ 0 ≤ a := by simp only [le_iff_eq_or_lt, inv_pos, zero_eq_inv]

Nonnegativity of Inverse in Division Monoid

Informal description

For any element $a$ in a division monoid, the inverse $a^{-1}$ is nonnegative if and only if $a$ itself is nonnegative, i.e., $0 \leq a^{-1} \leftrightarrow 0 \leq a$.

div_nonpos_of_nonpos_of_nonneg theorem

(ha : a ≤ 0) (hb : 0 ≤ b) : a / b ≤ 0

Full source

lemma div_nonpos_of_nonpos_of_nonneg (ha : a ≤ 0) (hb : 0 ≤ b) : a / b ≤ 0 := by
  rw [div_eq_mul_inv]; exact mul_nonpos_of_nonpos_of_nonneg ha (Right.inv_nonneg.2 hb)

Nonpositivity of Quotient of Nonpositive and Nonnegative Elements under Right Monotonicity

Informal description

Let $\alpha$ be a preorder with a division operation where right multiplication by nonnegative elements is monotone. Then for any nonpositive element $a \in \alpha$ (i.e., $a \leq 0$) and any nonnegative element $b \in \alpha$ (i.e., $b \geq 0$), their quotient $a / b$ is nonpositive, i.e., $a / b \leq 0$.

le_mul_inv_iff₀ theorem

(hc : 0 < c) : a ≤ b * c⁻¹ ↔ a * c ≤ b

Full source

/-- See `le_mul_inv_iff₀'` for a version with multiplication on the other side. -/
lemma le_mul_inv_iff₀ (hc : 0 < c) : a ≤ b * c⁻¹ ↔ a * c ≤ b := by
  rw [← mul_le_mul_iff_of_pos_right hc, inv_mul_cancel_right₀ hc.ne']

Inequality Equivalence under Right Multiplication by Positive Inverse: $a \leq b/c \leftrightarrow a \cdot c \leq b$

Informal description

For any elements $a$, $b$, and $c$ in a division monoid with $c > 0$, the inequality $a \leq b \cdot c^{-1}$ holds if and only if $a \cdot c \leq b$.

mul_inv_le_iff₀ theorem

(hc : 0 < c) : b * c⁻¹ ≤ a ↔ b ≤ a * c

Full source

/-- See `mul_inv_le_iff₀'` for a version with multiplication on the other side. -/
lemma mul_inv_le_iff₀ (hc : 0 < c) : b * c⁻¹ ≤ a ↔ b ≤ a * c := by
  rw [← mul_le_mul_iff_of_pos_right hc, inv_mul_cancel_right₀ hc.ne']

Inequality Equivalence for Multiplication by Inverse: $b \cdot c^{-1} \leq a \leftrightarrow b \leq a \cdot c$

Informal description

For any positive element $c$ in a group with zero (i.e., $0 < c$), the inequality $b \cdot c^{-1} \leq a$ holds if and only if $b \leq a \cdot c$.

lt_mul_inv_iff₀ theorem

(hc : 0 < c) : a < b * c⁻¹ ↔ a * c < b

Full source

/-- See `lt_mul_inv_iff₀'` for a version with multiplication on the other side. -/
lemma lt_mul_inv_iff₀ (hc : 0 < c) : a < b * c⁻¹ ↔ a * c < b := by
  rw [← mul_lt_mul_iff_of_pos_right hc, inv_mul_cancel_right₀ hc.ne']

Inequality involving multiplication and inverse: $a < b/c \leftrightarrow a \cdot c < b$ for $c > 0$

Informal description

For any elements $a, b, c$ in a group with zero $G_0$, if $0 < c$, then $a < b * c^{-1}$ if and only if $a * c < b$.

mul_inv_lt_iff₀ theorem

(hc : 0 < c) : b * c⁻¹ < a ↔ b < a * c

Full source

/-- See `mul_inv_lt_iff₀'` for a version with multiplication on the other side. -/
lemma mul_inv_lt_iff₀ (hc : 0 < c) : b * c⁻¹ < a ↔ b < a * c := by
  rw [← mul_lt_mul_iff_of_pos_right hc, inv_mul_cancel_right₀ hc.ne']

Inequality Involving Multiplication and Inverse in a Group with Zero: $b \cdot c^{-1} < a \leftrightarrow b < a \cdot c$

Informal description

For any positive element $c$ in a group with zero, the inequality $b \cdot c^{-1} < a$ holds if and only if $b < a \cdot c$.

le_div_iff₀ theorem

(hc : 0 < c) : a ≤ b / c ↔ a * c ≤ b

Full source

/-- See `le_div_iff₀'` for a version with multiplication on the other side. -/
lemma le_div_iff₀ (hc : 0 < c) : a ≤ b / c ↔ a * c ≤ b := by
  rw [div_eq_mul_inv, le_mul_inv_iff₀ hc]

Inequality Equivalence under Division by Positive Element: $a \leq b/c \leftrightarrow a \cdot c \leq b$

Informal description

For any elements $a$, $b$, and $c$ in a division monoid with $c > 0$, the inequality $a \leq b / c$ holds if and only if $a \cdot c \leq b$.

div_le_iff₀ theorem

(hc : 0 < c) : b / c ≤ a ↔ b ≤ a * c

Full source

/-- See `div_le_iff₀'` for a version with multiplication on the other side. -/
lemma div_le_iff₀ (hc : 0 < c) : b / c ≤ a ↔ b ≤ a * c := by
  rw [div_eq_mul_inv, mul_inv_le_iff₀ hc]

Division Inequality Equivalence: $\frac{b}{c} \leq a \leftrightarrow b \leq a \cdot c$

Informal description

For any positive element $c$ in a group with zero, the inequality $\frac{b}{c} \leq a$ holds if and only if $b \leq a \cdot c$.

lt_div_iff₀ theorem

(hc : 0 < c) : a < b / c ↔ a * c < b

Full source

/-- See `lt_div_iff₀'` for a version with multiplication on the other side. -/
lemma lt_div_iff₀ (hc : 0 < c) : a < b / c ↔ a * c < b := by
  rw [div_eq_mul_inv, lt_mul_inv_iff₀ hc]

Inequality equivalence: $a < b/c \leftrightarrow a \cdot c < b$ for $c > 0$

Informal description

For any elements $a, b, c$ in a group with zero, if $0 < c$, then $a < b / c$ if and only if $a \cdot c < b$.

div_lt_iff₀ theorem

(hc : 0 < c) : b / c < a ↔ b < a * c

Full source

/-- See `div_lt_iff₀'` for a version with multiplication on the other side. -/
lemma div_lt_iff₀ (hc : 0 < c) : b / c < a ↔ b < a * c := by
  rw [div_eq_mul_inv, mul_inv_lt_iff₀ hc]

Division Inequality in a Group with Zero: $b / c < a \leftrightarrow b < a \cdot c$

Informal description

For any positive element $c$ in a group with zero, the inequality $b / c < a$ holds if and only if $b < a \cdot c$.

div_le_div_iff_of_pos_right theorem

(hc : 0 < c) : a / c ≤ b / c ↔ a ≤ b

Full source

lemma div_le_div_iff_of_pos_right (hc : 0 < c) : a / c ≤ b / c ↔ a ≤ b := by
  rw [div_le_iff₀ hc, div_mul_cancel₀ _ hc.ne']

Division Preserves Order for Positive Elements: $\frac{a}{c} \leq \frac{b}{c} \leftrightarrow a \leq b$

Informal description

For any positive element $c$ in a group with zero, the inequality $\frac{a}{c} \leq \frac{b}{c}$ holds if and only if $a \leq b$.

div_lt_div_iff_of_pos_right theorem

(hc : 0 < c) : a / c < b / c ↔ a < b

Full source

lemma div_lt_div_iff_of_pos_right (hc : 0 < c) : a / c < b / c ↔ a < b := by
  rw [div_lt_iff₀ hc, div_mul_cancel₀ _ hc.ne']

Division Preserves Strict Order for Positive Elements: $a / c 0$

Informal description

For any positive element $c$ in a group with zero, the inequality $a / c < b / c$ holds if and only if $a < b$.

inv_le_iff_one_le_mul₀ theorem

(ha : 0 < a) : a⁻¹ ≤ b ↔ 1 ≤ b * a

Full source

/-- See `inv_le_iff_one_le_mul₀'` for a version with multiplication on the other side. -/
lemma inv_le_iff_one_le_mul₀ (ha : 0 < a) : a⁻¹a⁻¹ ≤ b ↔ 1 ≤ b * a := by
  rw [← mul_inv_le_iff₀ ha, one_mul]

Inverse Inequality Equivalence: $a^{-1} \leq b \leftrightarrow 1 \leq b \cdot a$ for $a > 0$

Informal description

For any positive element $a$ in a group with zero (i.e., $0 < a$), the inequality $a^{-1} \leq b$ holds if and only if $1 \leq b \cdot a$.

inv_lt_iff_one_lt_mul₀ theorem

(ha : 0 < a) : a⁻¹ < b ↔ 1 < b * a

Full source

/-- See `inv_lt_iff_one_lt_mul₀'` for a version with multiplication on the other side. -/
lemma inv_lt_iff_one_lt_mul₀ (ha : 0 < a) : a⁻¹a⁻¹ < b ↔ 1 < b * a := by
  rw [← mul_inv_lt_iff₀ ha, one_mul]

Inverse Inequality: $a^{-1} 0$

Informal description

For any positive element $a$ in a group with zero, the inequality $a^{-1} < b$ holds if and only if $1 < b \cdot a$.

one_le_div₀ theorem

(hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a

Full source

lemma one_le_div₀ (hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a := by rw [le_div_iff₀ hb, one_mul]

Inequality Equivalence for Division by Positive Element: $1 \leq a/b \leftrightarrow b \leq a$

Informal description

For any positive element $b$ in a division monoid (i.e., $0 < b$), the inequality $1 \leq a / b$ holds if and only if $b \leq a$.

div_le_one₀ theorem

(hb : 0 < b) : a / b ≤ 1 ↔ a ≤ b

Full source

lemma div_le_one₀ (hb : 0 < b) : a / b ≤ 1 ↔ a ≤ b := by rw [div_le_iff₀ hb, one_mul]

Division Inequality: $\frac{a}{b} \leq 1 \leftrightarrow a \leq b$ for $b > 0$

Informal description

For any positive element $b$ in a group with zero, the inequality $\frac{a}{b} \leq 1$ holds if and only if $a \leq b$.

mul_le_of_le_mul_inv₀ theorem

(hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ b * c⁻¹) : a * c ≤ b

Full source

/-- One direction of `le_mul_inv_iff₀` where `c` is allowed to be `0` (but `b` must be nonnegative).
-/
lemma mul_le_of_le_mul_inv₀ (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ b * c⁻¹) : a * c ≤ b := by
  obtain rfl | hc := hc.eq_or_lt
  · simpa using hb
  · rwa [le_mul_inv_iff₀ hc] at h

Inequality Implication under Right Multiplication by Nonnegative Inverse: $a \leq b/c \implies a \cdot c \leq b$

Informal description

For any elements $a$, $b$, and $c$ in a division monoid with $b \geq 0$ and $c \geq 0$, if $a \leq b \cdot c^{-1}$, then $a \cdot c \leq b$.

mul_inv_le_of_le_mul₀ theorem

(hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ c * b) : a * b⁻¹ ≤ c

Full source

/-- One direction of `mul_inv_le_iff₀` where `b` is allowed to be `0` (but `c` must be nonnegative).
-/
lemma mul_inv_le_of_le_mul₀ (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ c * b) : a * b⁻¹ ≤ c := by
  obtain rfl | hb := hb.eq_or_lt
  · simp [hc]
  · rwa [mul_inv_le_iff₀ hb]

Inequality for Multiplication by Inverse: $a \leq c \cdot b$ implies $a \cdot b^{-1} \leq c$

Informal description

For any nonnegative elements $b$ and $c$ in a group with zero (i.e., $0 \leq b$ and $0 \leq c$), if $a \leq c \cdot b$, then $a \cdot b^{-1} \leq c$.

mul_le_of_le_div₀ theorem

(hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ b / c) : a * c ≤ b

Full source

/-- One direction of `le_div_iff₀` where `c` is allowed to be `0` (but `b` must be nonnegative). -/
lemma mul_le_of_le_div₀ (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ b / c) : a * c ≤ b :=
  mul_le_of_le_mul_inv₀ hb hc (div_eq_mul_inv b _ ▸ h)

Inequality Implication under Right Multiplication by Nonnegative Divisor: $a \leq b/c \implies a \cdot c \leq b$

Informal description

For any elements $a$, $b$, and $c$ in a division monoid with $b \geq 0$ and $c \geq 0$, if $a \leq b / c$, then $a \cdot c \leq b$.

div_le_of_le_mul₀ theorem

(hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ c * b) : a / b ≤ c

Full source

/-- One direction of `div_le_iff₀` where `b` is allowed to be `0` (but `c` must be nonnegative). -/
lemma div_le_of_le_mul₀ (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ c * b) : a / b ≤ c :=
  div_eq_mul_inv a _ ▸ mul_inv_le_of_le_mul₀ hb hc h

Division Inequality: $a \leq c \cdot b$ implies $a / b \leq c$ for nonnegative $b, c$

Informal description

For any nonnegative elements $b$ and $c$ in a group with zero (i.e., $0 \leq b$ and $0 \leq c$), if $a \leq c \cdot b$, then $a / b \leq c$.

mul_inv_le_one_of_le₀ theorem

[ZeroLEOneClass G₀] (h : a ≤ b) (hb : 0 ≤ b) : a * b⁻¹ ≤ 1

Full source

@[bound]
lemma mul_inv_le_one_of_le₀ [ZeroLEOneClass G₀] (h : a ≤ b) (hb : 0 ≤ b) : a * b⁻¹ ≤ 1 :=
  mul_inv_le_of_le_mul₀ hb zero_le_one <| by rwa [one_mul]

Inequality for Product with Inverse: $a \leq b$ implies $a \cdot b^{-1} \leq 1$ when $b \geq 0$

Informal description

For any elements $a$ and $b$ in a group with zero $G_0$ where $0 \leq 1$ holds, if $a \leq b$ and $0 \leq b$, then $a \cdot b^{-1} \leq 1$.

div_le_one_of_le₀ theorem

[ZeroLEOneClass G₀] (h : a ≤ b) (hb : 0 ≤ b) : a / b ≤ 1

Full source

@[bound]
lemma div_le_one_of_le₀ [ZeroLEOneClass G₀] (h : a ≤ b) (hb : 0 ≤ b) : a / b ≤ 1 :=
  div_le_of_le_mul₀ hb zero_le_one <| by rwa [one_mul]

Division Inequality: $a \leq b$ implies $a / b \leq 1$ for nonnegative $b$

Informal description

For any elements $a$ and $b$ in a group with zero $G_0$ where $0 \leq 1$ holds, if $a \leq b$ and $0 \leq b$, then $a / b \leq 1$.

div_le_div_of_nonneg_right theorem

(hab : a ≤ b) (hc : 0 ≤ c) : a / c ≤ b / c

Full source

@[mono, gcongr, bound]
lemma div_le_div_of_nonneg_right (hab : a ≤ b) (hc : 0 ≤ c) : a / c ≤ b / c := by
  rw [div_eq_mul_inv a c, div_eq_mul_inv b c]
  exact mul_le_mul_of_nonneg_right hab (Right.inv_nonneg.2 hc)

Monotonicity of Division by Nonnegative Elements: $a \leq b \land c \geq 0 \implies a/c \leq b/c$

Informal description

For any elements $a, b, c$ in a preordered division monoid, if $a \leq b$ and $0 \leq c$, then $a / c \leq b / c$.

div_lt_div_of_pos_right theorem

(h : a < b) (hc : 0 < c) : a / c < b / c

Full source

@[gcongr, bound]
lemma div_lt_div_of_pos_right (h : a < b) (hc : 0 < c) : a / c < b / c := by
  rw [div_eq_mul_inv a c, div_eq_mul_inv b c]
  exact mul_lt_mul_of_pos_right h (Right.inv_pos.2 hc)

Strict Monotonicity of Right Division by Positive Elements: $a 0 \implies a/c < b/c$

Informal description

For any elements $a, b, c$ in a preordered division monoid, if $a < b$ and $0 < c$, then $a / c < b / c$.

inv_le_inv₀ theorem

(ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a

Full source

/-- See `inv_anti₀` for the implication from right-to-left with one fewer assumption. -/
lemma inv_le_inv₀ (ha : 0 < a) (hb : 0 < b) : a⁻¹a⁻¹ ≤ b⁻¹ ↔ b ≤ a := by
  rw [inv_le_iff_one_le_mul₀' ha, le_mul_inv_iff₀ hb, one_mul]

Inverse Order Reversal: $a^{-1} \leq b^{-1} \leftrightarrow b \leq a$ for $a, b > 0$

Informal description

For any positive elements $a$ and $b$ in a group with zero, the inequality $a^{-1} \leq b^{-1}$ holds if and only if $b \leq a$.

inv_lt_inv₀ theorem

(ha : 0 < a) (hb : 0 < b) : a⁻¹ < b⁻¹ ↔ b < a

Full source

/-- See `inv_strictAnti₀` for the implication from right-to-left with one fewer assumption. -/
lemma inv_lt_inv₀ (ha : 0 < a) (hb : 0 < b) : a⁻¹a⁻¹ < b⁻¹ ↔ b < a := by
  rw [inv_lt_iff_one_lt_mul₀' ha, lt_mul_inv_iff₀ hb, one_mul]

Inverse Inequality Equivalence: $a^{-1} < b^{-1} \leftrightarrow b < a$ for $a, b > 0$

Informal description

For any positive elements $a$ and $b$ in a group with zero, the inequality $a^{-1} < b^{-1}$ holds if and only if $b < a$.

inv_anti₀ theorem

(hb : 0 < b) (hba : b ≤ a) : a⁻¹ ≤ b⁻¹

Full source

@[gcongr, bound]
lemma inv_anti₀ (hb : 0 < b) (hba : b ≤ a) : a⁻¹ ≤ b⁻¹ := (inv_le_inv₀ (hb.trans_le hba) hb).2 hba

Antitonicity of Inverse for Positive Elements: $b \leq a \Rightarrow a^{-1} \leq b^{-1}$ when $b > 0$

Informal description

For any positive elements $a$ and $b$ in a group with zero, if $b \leq a$, then $a^{-1} \leq b^{-1}$.

inv_strictAnti₀ theorem

(hb : 0 < b) (hba : b < a) : a⁻¹ < b⁻¹

Full source

@[gcongr, bound]
lemma inv_strictAnti₀ (hb : 0 < b) (hba : b < a) : a⁻¹ < b⁻¹ :=
  (inv_lt_inv₀ (hb.trans hba) hb).2 hba

Strict Antitonicity of Inverse for Positive Elements: $b < a \Rightarrow a^{-1} < b^{-1}$ when $b > 0$

Informal description

For any positive elements $b$ and $a$ in a group with zero such that $b < a$, the inequality $a^{-1} < b^{-1}$ holds.

inv_le_comm₀ theorem

(ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b ↔ b⁻¹ ≤ a

Full source

/-- See also `inv_le_of_inv_le₀` for a one-sided implication with one fewer assumption. -/
lemma inv_le_comm₀ (ha : 0 < a) (hb : 0 < b) : a⁻¹a⁻¹ ≤ b ↔ b⁻¹ ≤ a := by
  rw [← inv_le_inv₀ hb (inv_pos.2 ha), inv_inv]

Inverse-Order Commutation: $a^{-1} \leq b \leftrightarrow b^{-1} \leq a$ for $a, b > 0$

Informal description

For any positive elements $a$ and $b$ in a group with zero, the inequality $a^{-1} \leq b$ holds if and only if $b^{-1} \leq a$.

inv_lt_comm₀ theorem

(ha : 0 < a) (hb : 0 < b) : a⁻¹ < b ↔ b⁻¹ < a

Full source

/-- See also `inv_lt_of_inv_lt₀` for a one-sided implication with one fewer assumption. -/
lemma inv_lt_comm₀ (ha : 0 < a) (hb : 0 < b) : a⁻¹a⁻¹ < b ↔ b⁻¹ < a := by
  rw [← inv_lt_inv₀ hb (inv_pos.2 ha), inv_inv]

Inverse Inequality Commutation: $a^{-1} 0$

Informal description

For any positive elements $a$ and $b$ in a group with zero, the inequality $a^{-1} < b$ holds if and only if $b^{-1} < a$.

inv_le_of_inv_le₀ theorem

(ha : 0 < a) (h : a⁻¹ ≤ b) : b⁻¹ ≤ a

Full source

lemma inv_le_of_inv_le₀ (ha : 0 < a) (h : a⁻¹ ≤ b) : b⁻¹ ≤ a :=
  (inv_le_comm₀ ha <| (inv_pos.2 ha).trans_le h).1 h

Inverse Inequality Implication: $a^{-1} \leq b \to b^{-1} \leq a$ for $a > 0$

Informal description

For any positive element $a$ in a group with zero, if the inverse of $a$ is less than or equal to an element $b$, then the inverse of $b$ is less than or equal to $a$. That is, if $0 < a$ and $a^{-1} \leq b$, then $b^{-1} \leq a$.

inv_lt_of_inv_lt₀ theorem

(ha : 0 < a) (h : a⁻¹ < b) : b⁻¹ < a

Full source

lemma inv_lt_of_inv_lt₀ (ha : 0 < a) (h : a⁻¹ < b) : b⁻¹ < a :=
  (inv_lt_comm₀ ha <| (inv_pos.2 ha).trans h).1 h

Inverse Inequality Implication: $a^{-1} 0$

Informal description

For any positive element $a$ in a group with zero, if $a^{-1} < b$, then $b^{-1} < a$.

le_inv_comm₀ theorem

(ha : 0 < a) (hb : 0 < b) : a ≤ b⁻¹ ↔ b ≤ a⁻¹

Full source

/-- See also `le_inv_of_le_inv₀` for a one-sided implication with one fewer assumption. -/
lemma le_inv_comm₀ (ha : 0 < a) (hb : 0 < b) : a ≤ b⁻¹ ↔ b ≤ a⁻¹ := by
  rw [← inv_le_inv₀ (inv_pos.2 hb) ha, inv_inv]

Order Reversal of Inverse Elements: $a \leq b^{-1} \leftrightarrow b \leq a^{-1}$ for $a, b > 0$

Informal description

For any positive elements $a$ and $b$ in a group with zero, the inequality $a \leq b^{-1}$ holds if and only if $b \leq a^{-1}$.

lt_inv_comm₀ theorem

(ha : 0 < a) (hb : 0 < b) : a < b⁻¹ ↔ b < a⁻¹

Full source

/-- See also `lt_inv_of_lt_inv₀` for a one-sided implication with one fewer assumption. -/
lemma lt_inv_comm₀ (ha : 0 < a) (hb : 0 < b) : a < b⁻¹ ↔ b < a⁻¹ := by
  rw [← inv_lt_inv₀ (inv_pos.2 hb) ha, inv_inv]

Strict Inverse Inequality Commutation: $a < b^{-1} \leftrightarrow b < a^{-1}$ for $a, b > 0$

Informal description

For any positive elements $a$ and $b$ in a group with zero, the inequality $a < b^{-1}$ holds if and only if $b < a^{-1}$.

le_inv_of_le_inv₀ theorem

(ha : 0 < a) (h : a ≤ b⁻¹) : b ≤ a⁻¹

Full source

lemma le_inv_of_le_inv₀ (ha : 0 < a) (h : a ≤ b⁻¹) : b ≤ a⁻¹ :=
  (le_inv_comm₀ ha <| inv_pos.1 <| ha.trans_le h).1 h

Order Reversal of Inverse Elements: $a \leq b^{-1} \implies b \leq a^{-1}$ for $a > 0$

Informal description

For any positive element $a$ in a group with zero, if $a \leq b^{-1}$, then $b \leq a^{-1}$.

lt_inv_of_lt_inv₀ theorem

(ha : 0 < a) (h : a < b⁻¹) : b < a⁻¹

Full source

lemma lt_inv_of_lt_inv₀ (ha : 0 < a) (h : a < b⁻¹) : b < a⁻¹ :=
  (lt_inv_comm₀ ha <| inv_pos.1 <| ha.trans h).1 h

Strict Inverse Order Reversal: $a < b^{-1} \implies b < a^{-1}$ for $a > 0$

Informal description

For any positive element $a$ in a group with zero, if $a < b^{-1}$, then $b < a^{-1}$.

div_le_div_iff_of_pos_left theorem

(ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a / b ≤ a / c ↔ c ≤ b

Full source

lemma div_le_div_iff_of_pos_left (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
    a / b ≤ a / c ↔ c ≤ b := by
  simp only [div_eq_mul_inv, mul_le_mul_left ha, inv_le_inv₀ hb hc]

Division Inequality for Positive Elements: $\frac{a}{b} \leq \frac{a}{c} \leftrightarrow c \leq b$ when $a, b, c > 0$

Informal description

For any positive real numbers $a, b, c > 0$, the inequality $\frac{a}{b} \leq \frac{a}{c}$ holds if and only if $c \leq b$.

div_lt_div_iff_of_pos_left theorem

(ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a / b < a / c ↔ c < b

Full source

lemma div_lt_div_iff_of_pos_left (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a / b < a / c ↔ c < b :=
  lt_iff_lt_of_le_iff_le' (div_le_div_iff_of_pos_left ha hc hb)
    (div_le_div_iff_of_pos_left ha hb hc)

Strict Division Inequality for Positive Elements: $\frac{a}{b} < \frac{a}{c} \leftrightarrow c < b$ when $a, b, c > 0$

Informal description

For any positive real numbers $a, b, c > 0$, the strict inequality $\frac{a}{b} < \frac{a}{c}$ holds if and only if $c < b$.

div_le_div_of_nonneg_left theorem

(ha : 0 ≤ a) (hc : 0 < c) (h : c ≤ b) : a / b ≤ a / c

Full source

@[gcongr]
lemma div_le_div_of_nonneg_left (ha : 0 ≤ a) (hc : 0 < c) (h : c ≤ b) : a / b ≤ a / c := by
  rw [div_eq_mul_inv, div_eq_mul_inv]
  gcongr
  exacts [ha, hc]

Nonnegative Division Inequality: $c \leq b \Rightarrow a/b \leq a/c$ for $a \geq 0$, $c > 0$

Informal description

For any nonnegative element $a$ and positive elements $b, c$ in a preordered group with zero, if $c \leq b$, then the inequality $a / b \leq a / c$ holds.

div_lt_div_of_pos_left theorem

(ha : 0 < a) (hc : 0 < c) (h : c < b) : a / b < a / c

Full source

@[gcongr, bound]
lemma div_lt_div_of_pos_left (ha : 0 < a) (hc : 0 < c) (h : c < b) : a / b < a / c :=
  (div_lt_div_iff_of_pos_left ha (hc.trans h) hc).mpr h

Strict Division Inequality: $\frac{a}{b} < \frac{a}{c}$ when $a, c > 0$ and $c < b$

Informal description

For any positive real numbers $a, c$ and any real number $b$ such that $0 < a$, $0 < c$, and $c < b$, the inequality $\frac{a}{b} < \frac{a}{c}$ holds.

div_le_div₀ theorem

(hc : 0 ≤ c) (hac : a ≤ c) (hd : 0 < d) (hdb : d ≤ b) : a / b ≤ c / d

Full source

@[mono, gcongr, bound]
lemma div_le_div₀ (hc : 0 ≤ c) (hac : a ≤ c) (hd : 0 < d) (hdb : d ≤ b) : a / b ≤ c / d := by
  rw [div_eq_mul_inv, div_eq_mul_inv]
  exact mul_le_mul hac ((inv_le_inv₀ (hd.trans_le hdb) hd).2 hdb)
    (inv_nonneg.2 <| hd.le.trans hdb) hc

Division Inequality under Nonnegative Conditions: $a / b \leq c / d$

Informal description

For any elements $a, b, c, d$ in a division monoid with zero, if $0 \leq c$, $a \leq c$, $0 < d$, and $d \leq b$, then the inequality $a / b \leq c / d$ holds.

div_lt_div₀ theorem

(hac : a < c) (hdb : d ≤ b) (hc : 0 ≤ c) (hd : 0 < d) : a / b < c / d

Full source

@[gcongr]
lemma div_lt_div₀ (hac : a < c) (hdb : d ≤ b) (hc : 0 ≤ c) (hd : 0 < d) : a / b < c / d := by
  rw [div_eq_mul_inv, div_eq_mul_inv]
  apply mul_lt_mul hac (by gcongr; assumption) _ hc
  exact inv_pos.2 (hd.trans_le hdb)

Fraction Inequality under Partial Order: $\frac{a}{b} < \frac{c}{d}$ when $a < c$, $d \leq b$, $c \geq 0$, and $d > 0$

Informal description

For any elements $a, b, c, d$ in a division monoid with zero, if $a < c$, $d \leq b$, $0 \leq c$, and $0 < d$, then the inequality $\frac{a}{b} < \frac{c}{d}$ holds.

div_lt_div₀' theorem

(hac : a ≤ c) (hdb : d < b) (hc : 0 < c) (hd : 0 < d) : a / b < c / d

Full source

lemma div_lt_div₀' (hac : a ≤ c) (hdb : d < b) (hc : 0 < c) (hd : 0 < d) : a / b < c / d := by
  rw [div_eq_mul_inv, div_eq_mul_inv]
  exact mul_lt_mul' hac ((inv_lt_inv₀ (hd.trans hdb) hd).2 hdb)
    (inv_nonneg.2 <| hd.le.trans hdb.le) hc

Fraction Inequality under Partial Order: $\frac{a}{b} < \frac{c}{d}$ when $a \leq c$, $d < b$, and $c, d > 0$

Informal description

For elements $a, b, c, d$ in a division monoid with $0 < c$, $0 < d$, $a \leq c$, and $d < b$, the inequality $\frac{a}{b} < \frac{c}{d}$ holds.

inv_neg'' theorem

: a⁻¹ < 0 ↔ a < 0

Full source

@[simp] lemma inv_neg'' : a⁻¹a⁻¹ < 0 ↔ a < 0 := by
  have := PosMulMono.toPosMulReflectLT (α := G₀); simp only [← not_le, inv_nonneg]

Inverse Negativity Criterion: $a^{-1} < 0 \leftrightarrow a < 0$

Informal description

For any element $a$ in a division monoid, the inverse $a^{-1}$ is negative (i.e., $a^{-1} < 0$) if and only if $a$ itself is negative (i.e., $a < 0$).

inv_nonpos theorem

: a⁻¹ ≤ 0 ↔ a ≤ 0

Full source

@[simp] lemma inv_nonpos : a⁻¹a⁻¹ ≤ 0 ↔ a ≤ 0 := by
  have := PosMulMono.toPosMulReflectLT (α := G₀); simp only [← not_lt, inv_pos]

Inverse Nonpositivity Criterion: $a^{-1} \leq 0 \leftrightarrow a \leq 0$

Informal description

For any element $a$ in a division monoid, the inverse $a^{-1}$ is nonpositive (i.e., $a^{-1} \leq 0$) if and only if $a$ itself is nonpositive (i.e., $a \leq 0$).

one_div_neg theorem

: 1 / a < 0 ↔ a < 0

Full source

lemma one_div_neg : 1 / a < 0 ↔ a < 0 := one_div a ▸ inv_neg''

Reciprocal Negativity Criterion: $1/a < 0 \leftrightarrow a < 0$

Informal description

For any element $a$ in a division monoid, the reciprocal $1/a$ is negative (i.e., $1/a < 0$) if and only if $a$ itself is negative (i.e., $a < 0$).

one_div_nonpos theorem

: 1 / a ≤ 0 ↔ a ≤ 0

Full source

lemma one_div_nonpos : 1 / a ≤ 0 ↔ a ≤ 0 := one_div a ▸ inv_nonpos

Reciprocal Nonpositivity Criterion: $1/a \leq 0 \leftrightarrow a \leq 0$

Informal description

For any element $a$ in a division monoid, the reciprocal $1/a$ is nonpositive (i.e., $1/a \leq 0$) if and only if $a$ itself is nonpositive (i.e., $a \leq 0$).

div_nonpos_of_nonneg_of_nonpos theorem

(ha : 0 ≤ a) (hb : b ≤ 0) : a / b ≤ 0

Full source

lemma div_nonpos_of_nonneg_of_nonpos (ha : 0 ≤ a) (hb : b ≤ 0) : a / b ≤ 0 := by
  rw [div_eq_mul_inv]; exact mul_nonpos_of_nonneg_of_nonpos ha (inv_nonpos.2 hb)

Nonpositivity of Quotient of Nonnegative and Nonpositive Elements

Informal description

For any elements $a$ and $b$ in a division monoid, if $a$ is nonnegative ($a \geq 0$) and $b$ is nonpositive ($b \leq 0$), then their quotient $a / b$ is nonpositive, i.e., $a / b \leq 0$.

neg_of_div_neg_right theorem

(h : a / b < 0) (ha : 0 ≤ a) : b < 0

Full source

lemma neg_of_div_neg_right (h : a / b < 0) (ha : 0 ≤ a) : b < 0 :=
  have := PosMulMono.toPosMulReflectLT (α := G₀)
  lt_of_not_ge fun hb ↦ (div_nonneg ha hb).not_lt h

Negativity of Denominator from Negative Quotient with Nonnegative Numerator

Informal description

For any elements $a$ and $b$ in a division monoid, if $a / b < 0$ and $a \geq 0$, then $b < 0$.

neg_of_div_neg_left theorem

(h : a / b < 0) (hb : 0 ≤ b) : a < 0

Full source

lemma neg_of_div_neg_left (h : a / b < 0) (hb : 0 ≤ b) : a < 0 :=
  have := PosMulMono.toPosMulReflectLT (α := G₀)
  lt_of_not_ge fun ha ↦ (div_nonneg ha hb).not_lt h

Negativity of Dividend from Negative Quotient with Nonnegative Divisor

Informal description

For any elements $a$ and $b$ in a division monoid, if $a / b < 0$ and $b \geq 0$, then $a < 0$.

inv_lt_one_iff₀ theorem

: a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a

Full source

lemma inv_lt_one_iff₀ : a⁻¹a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a := by
  simp_rw [← not_le, one_le_inv_iff₀, not_and_or, not_lt]

Characterization of when $a^{-1} < 1$ in a division monoid with zero

Informal description

For any element $a$ in a division monoid with zero, the inverse of $a$ is less than $1$ if and only if either $a \leq 0$ or $1 < a$.

inv_le_one_iff₀ theorem

: a⁻¹ ≤ 1 ↔ a ≤ 0 ∨ 1 ≤ a

Full source

lemma inv_le_one_iff₀ : a⁻¹a⁻¹ ≤ 1 ↔ a ≤ 0 ∨ 1 ≤ a := by
  simp only [← not_lt, one_lt_inv_iff₀, not_and_or]

Inverse Inequality: $a^{-1} \leq 1$ iff $a \leq 0$ or $1 \leq a$

Informal description

For any nonzero element $a$ in a linear ordered commutative group with zero, the inequality $a^{-1} \leq 1$ holds if and only if either $a \leq 0$ or $1 \leq a$.

zpow_right_injective₀ theorem

(ha₀ : 0 < a) (ha₁ : a ≠ 1) : Injective fun n : ℤ ↦ a ^ n

Full source

lemma zpow_right_injective₀ (ha₀ : 0 < a) (ha₁ : a ≠ 1) : Injective fun n : ℤ ↦ a ^ n := by
  obtain ha₁ | ha₁ := ha₁.lt_or_lt
  · exact (zpow_right_strictAnti₀ ha₀ ha₁).injective
  · exact (zpow_right_strictMono₀ ha₁).injective

Injectivity of Integer Powers for $0 < a \neq 1$

Informal description

For any element $a$ in a division monoid with $0 < a$ and $a \neq 1$, the integer power function $n \mapsto a^n$ is injective.

zpow_right_inj₀ theorem

(ha₀ : 0 < a) (ha₁ : a ≠ 1) : a ^ m = a ^ n ↔ m = n

Full source

@[simp] lemma zpow_right_inj₀ (ha₀ : 0 < a) (ha₁ : a ≠ 1) : a ^ m = a ^ n ↔ m = n :=
  (zpow_right_injective₀ ha₀ ha₁).eq_iff

Injectivity of Integer Powers: $a^m = a^n \leftrightarrow m = n$ for $0 < a \neq 1$

Informal description

For any element $a$ in a division monoid with $0 < a$ and $a \neq 1$, the equality $a^m = a^n$ holds if and only if $m = n$.

zpow_eq_one_iff_right₀ theorem

(ha₀ : 0 ≤ a) (ha₁ : a ≠ 1) {n : ℤ} : a ^ n = 1 ↔ n = 0

Full source

lemma zpow_eq_one_iff_right₀ (ha₀ : 0 ≤ a) (ha₁ : a ≠ 1) {n : ℤ} : a ^ n = 1 ↔ n = 0 := by
  obtain rfl | ha₀ := ha₀.eq_or_lt
  · exact zero_zpow_eq_one₀
  simpa using zpow_right_inj₀ ha₀ ha₁ (n := 0)

Integer Power Equals One if and only if Exponent is Zero for $0 \leq a \neq 1$

Informal description

For any element $a$ in a division monoid with $0 \leq a$ and $a \neq 1$, and for any integer $n$, the equality $a^n = 1$ holds if and only if $n = 0$.

mul_div_mul_left_le theorem

(h : 0 ≤ a / b) : c * a / (c * b) ≤ a / b

Full source

/-- Equality holds when `c ≠ 0`. See `mul_div_mul_left`. -/
lemma mul_div_mul_left_le (h : 0 ≤ a / b) : c * a / (c * b) ≤ a / b := by
  obtain rfl | hc := eq_or_ne c 0
  · simpa
  · rw [mul_div_mul_left _ _ hc]

Inequality for Left Multiplication in Division under Nonnegative Quotient

Informal description

For any elements $a$, $b$, and $c$ in a division algebra, if $0 \leq a / b$, then $(c \cdot a) / (c \cdot b) \leq a / b$.

le_mul_div_mul_left theorem

(h : a / b ≤ 0) : a / b ≤ c * a / (c * b)

Full source

/-- Equality holds when `c ≠ 0`. See `mul_div_mul_left`. -/
lemma le_mul_div_mul_left (h : a / b ≤ 0) : a / b ≤ c * a / (c * b) := by
  obtain rfl | hc := eq_or_ne c 0
  · simpa
  · rw [mul_div_mul_left _ _ hc]

Inequality for Left Multiplication in Division under Nonpositive Condition

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered commutative group with zero, if $a / b \leq 0$, then $a / b \leq (c \cdot a) / (c \cdot b)$.

le_inv_mul_iff₀' theorem

(hc : 0 < c) : a ≤ c⁻¹ * b ↔ c * a ≤ b

Full source

/-- See `le_inv_mul_iff₀` for a version with multiplication on the other side. -/
lemma le_inv_mul_iff₀' (hc : 0 < c) : a ≤ c⁻¹ * b ↔ c * a ≤ b := by
  rw [le_inv_mul_iff₀ hc, mul_comm]

Inequality Equivalence under Left Multiplication by Inverse: $a \leq c^{-1} \cdot b \leftrightarrow c \cdot a \leq b$ for $c > 0$

Informal description

For any positive element $c$ in a group with zero, the inequality $a \leq c^{-1} \cdot b$ holds if and only if $c \cdot a \leq b$.

inv_mul_le_iff₀' theorem

(hc : 0 < c) : c⁻¹ * b ≤ a ↔ b ≤ a * c

Full source

/-- See `inv_mul_le_iff₀` for a version with multiplication on the other side. -/
lemma inv_mul_le_iff₀' (hc : 0 < c) : c⁻¹c⁻¹ * b ≤ a ↔ b ≤ a * c := by
  rw [inv_mul_le_iff₀ hc, mul_comm]

Inverse Multiplication Inequality (Right Variant): $c^{-1}b \leq a \leftrightarrow b \leq a c$ for $c > 0$

Informal description

For any positive element $c$ in a group with zero, the inequality $c^{-1} \cdot b \leq a$ holds if and only if $b \leq a \cdot c$.

le_mul_inv_iff₀' theorem

(hc : 0 < c) : a ≤ b * c⁻¹ ↔ c * a ≤ b

Full source

/-- See `le_mul_inv_iff₀` for a version with multiplication on the other side. -/
lemma le_mul_inv_iff₀' (hc : 0 < c) : a ≤ b * c⁻¹ ↔ c * a ≤ b := by
  rw [le_mul_inv_iff₀ hc, mul_comm]

Inequality Equivalence under Left Multiplication by Positive Inverse: $a \leq b/c \leftrightarrow c \cdot a \leq b$

Informal description

For any elements $a$, $b$, and $c$ in a division monoid with $c > 0$, the inequality $a \leq b \cdot c^{-1}$ holds if and only if $c \cdot a \leq b$.

mul_inv_le_iff₀' theorem

(hc : 0 < c) : b * c⁻¹ ≤ a ↔ b ≤ c * a

Full source

/-- See `mul_inv_le_iff₀` for a version with multiplication on the other side. -/
lemma mul_inv_le_iff₀' (hc : 0 < c) : b * c⁻¹ ≤ a ↔ b ≤ c * a := by
  rw [mul_inv_le_iff₀ hc, mul_comm]

Inequality Equivalence for Multiplication by Inverse: $b \cdot c^{-1} \leq a \leftrightarrow b \leq c \cdot a$

Informal description

For any positive element $c$ in a group with zero (i.e., $0 < c$), the inequality $b \cdot c^{-1} \leq a$ holds if and only if $b \leq c \cdot a$.

div_le_div_iff₀ theorem

(hb : 0 < b) (hd : 0 < d) : a / b ≤ c / d ↔ a * d ≤ c * b

Full source

lemma div_le_div_iff₀ (hb : 0 < b) (hd : 0 < d) : a / b ≤ c / d ↔ a * d ≤ c * b := by
  rw [div_le_iff₀ hb, ← mul_div_right_comm, le_div_iff₀ hd]

Division Inequality Equivalence: $\frac{a}{b} \leq \frac{c}{d} \leftrightarrow a \cdot d \leq c \cdot b$ for $b, d > 0$

Informal description

For any positive elements $b$ and $d$ in a group with zero, the inequality $\frac{a}{b} \leq \frac{c}{d}$ holds if and only if $a \cdot d \leq c \cdot b$.

le_div_iff₀' theorem

(hc : 0 < c) : a ≤ b / c ↔ c * a ≤ b

Full source

/-- See `le_div_iff₀` for a version with multiplication on the other side. -/
lemma le_div_iff₀' (hc : 0 < c) : a ≤ b / c ↔ c * a ≤ b := by
  rw [le_div_iff₀ hc, mul_comm]

Inequality Equivalence under Division by Positive Element: $a \leq b/c \leftrightarrow c \cdot a \leq b$

Informal description

For any elements $a$, $b$, and $c$ in a division monoid with $c > 0$, the inequality $a \leq b / c$ holds if and only if $c \cdot a \leq b$.

div_le_iff₀' theorem

(hc : 0 < c) : b / c ≤ a ↔ b ≤ c * a

Full source

/-- See `div_le_iff₀` for a version with multiplication on the other side. -/
lemma div_le_iff₀' (hc : 0 < c) : b / c ≤ a ↔ b ≤ c * a := by
  rw [div_le_iff₀ hc, mul_comm]

Division Inequality Equivalence (Right Multiplication): $\frac{b}{c} \leq a \leftrightarrow b \leq c \cdot a$

Informal description

For any positive element $c$ in a group with zero, the inequality $\frac{b}{c} \leq a$ holds if and only if $b \leq c \cdot a$.

le_div_comm₀ theorem

(ha : 0 < a) (hc : 0 < c) : a ≤ b / c ↔ c ≤ b / a

Full source

lemma le_div_comm₀ (ha : 0 < a) (hc : 0 < c) : a ≤ b / c ↔ c ≤ b / a := by
  rw [le_div_iff₀ ha, le_div_iff₀' hc]

Division Inequality Commutation: $a \leq b/c \leftrightarrow c \leq b/a$ for positive $a,c$

Informal description

For any positive elements $a$ and $c$ in a group with zero, the inequality $a \leq b / c$ holds if and only if $c \leq b / a$.

div_le_comm₀ theorem

(hb : 0 < b) (hc : 0 < c) : a / b ≤ c ↔ a / c ≤ b

Full source

lemma div_le_comm₀ (hb : 0 < b) (hc : 0 < c) : a / b ≤ c ↔ a / c ≤ b := by
  rw [div_le_iff₀ hb, div_le_iff₀' hc]

Division Inequality Commutativity: $\frac{a}{b} \leq c \leftrightarrow \frac{a}{c} \leq b$ for $b, c > 0$

Informal description

For any positive elements $b$ and $c$ in a group with zero, the inequality $\frac{a}{b} \leq c$ holds if and only if $\frac{a}{c} \leq b$.

lt_inv_mul_iff₀' theorem

(hc : 0 < c) : a < c⁻¹ * b ↔ a * c < b

Full source

/-- See `lt_inv_mul_iff₀` for a version with multiplication on the other side. -/
lemma lt_inv_mul_iff₀' (hc : 0 < c) : a < c⁻¹ * b ↔ a * c < b := by
  rw [lt_inv_mul_iff₀ hc, mul_comm]

Inequality Equivalence under Right Multiplication by Inverse in Group with Zero

Informal description

For any positive element $c$ in a group with zero, the inequality $a < c^{-1} \cdot b$ holds if and only if $a \cdot c < b$.

inv_mul_lt_iff₀' theorem

(hc : 0 < c) : c⁻¹ * b < a ↔ b < a * c

Full source

/-- See `inv_mul_lt_iff₀` for a version with multiplication on the other side. -/
lemma inv_mul_lt_iff₀' (hc : 0 < c) : c⁻¹c⁻¹ * b < a ↔ b < a * c := by
  rw [inv_mul_lt_iff₀ hc, mul_comm]

Inverse Multiplication Inequality (Right Variant): $c^{-1}b < a \leftrightarrow b < a c$ for $c > 0$

Informal description

For any positive element $c$ in a group with zero, the inequality $c^{-1} \cdot b < a$ holds if and only if $b < a \cdot c$.

lt_mul_inv_iff₀' theorem

(hc : 0 < c) : a < b * c⁻¹ ↔ c * a < b

Full source

/-- See `lt_mul_inv_iff₀` for a version with multiplication on the other side. -/
lemma lt_mul_inv_iff₀' (hc : 0 < c) : a < b * c⁻¹ ↔ c * a < b := by
  rw [lt_mul_inv_iff₀ hc, mul_comm]

Inequality involving left multiplication and inverse: $a < b/c \leftrightarrow c \cdot a < b$ for $c > 0$

Informal description

For any elements $a, b, c$ in a group with zero $G_0$, if $0 < c$, then $a < b \cdot c^{-1}$ if and only if $c \cdot a < b$.

mul_inv_lt_iff₀' theorem

(hc : 0 < c) : b * c⁻¹ < a ↔ b < c * a

Full source

/-- See `mul_inv_lt_iff₀` for a version with multiplication on the other side. -/
lemma mul_inv_lt_iff₀' (hc : 0 < c) : b * c⁻¹ < a ↔ b < c * a := by
  rw [mul_inv_lt_iff₀ hc, mul_comm]

Inequality Involving Right Multiplication and Inverse: $b \cdot c^{-1} < a \leftrightarrow b < c \cdot a$

Informal description

For any positive element $c$ in a group with zero, the inequality $b \cdot c^{-1} < a$ holds if and only if $b < c \cdot a$.

div_lt_div_iff₀ theorem

(hb : 0 < b) (hd : 0 < d) : a / b < c / d ↔ a * d < c * b

Full source

lemma div_lt_div_iff₀ (hb : 0 < b) (hd : 0 < d) : a / b < c / d ↔ a * d < c * b := by
  rw [div_lt_iff₀ hb, ← mul_div_right_comm, lt_div_iff₀ hd]

Fraction Inequality Equivalence: $\frac{a}{b} < \frac{c}{d} \leftrightarrow a \cdot d < c \cdot b$ for $b, d > 0$

Informal description

For any positive elements $b$ and $d$ in a group with zero, the inequality $\frac{a}{b} < \frac{c}{d}$ holds if and only if $a \cdot d < c \cdot b$.

lt_div_iff₀' theorem

(hc : 0 < c) : a < b / c ↔ c * a < b

Full source

/-- See `lt_div_iff₀` for a version with multiplication on the other side. -/
lemma lt_div_iff₀' (hc : 0 < c) : a < b / c ↔ c * a < b := by
  rw [lt_div_iff₀ hc, mul_comm]

Inequality equivalence: $a < b/c \leftrightarrow c \cdot a < b$ for $c > 0$

Informal description

For any elements $a, b, c$ in a group with zero, if $0 < c$, then $a < b / c$ if and only if $c \cdot a < b$.

div_lt_iff₀' theorem

(hc : 0 < c) : b / c < a ↔ b < c * a

Full source

/-- See `div_lt_iff₀` for a version with multiplication on the other side. -/
lemma div_lt_iff₀' (hc : 0 < c) : b / c < a ↔ b < c * a := by
  rw [div_lt_iff₀ hc, mul_comm]

Division Inequality with Right Multiplication: $b / c < a \leftrightarrow b < c \cdot a$

Informal description

For any positive element $c$ in a group with zero, the inequality $b / c < a$ holds if and only if $b < c \cdot a$.

lt_div_comm₀ theorem

(ha : 0 < a) (hc : 0 < c) : a < b / c ↔ c < b / a

Full source

lemma lt_div_comm₀ (ha : 0 < a) (hc : 0 < c) : a < b / c ↔ c < b / a := by
  rw [lt_div_iff₀ ha, lt_div_iff₀' hc]

Inequality Equivalence: $a < b/c \leftrightarrow c < b/a$ for Positive $a, c$

Informal description

For any elements $a, b, c$ in a group with zero such that $0 < a$ and $0 < c$, the inequality $a < b / c$ holds if and only if $c < b / a$.

div_lt_comm₀ theorem

(hb : 0 < b) (hc : 0 < c) : a / b < c ↔ a / c < b

Full source

lemma div_lt_comm₀ (hb : 0 < b) (hc : 0 < c) : a / b < c ↔ a / c < b := by
  rw [div_lt_iff₀ hb, div_lt_iff₀' hc]

Division Inequality Commutativity: $a / b < c \leftrightarrow a / c < b$ for Positive Elements

Informal description

For any positive elements $b$ and $c$ in a group with zero, the inequality $a / b < c$ holds if and only if $a / c < b$.