Mathlib.Algebra.Order.Group.Unbundled.Basic

Left.inv_le_one_iff theorem

: a⁻¹ ≤ 1 ↔ 1 ≤ a

Full source

/-- Uses `left` co(ntra)variant. -/
@[to_additive (attr := simp) "Uses `left` co(ntra)variant."]
theorem Left.inv_le_one_iff : a⁻¹a⁻¹ ≤ 1 ↔ 1 ≤ a := by
  rw [← mul_le_mul_iff_left a]
  simp

Inverse Inequality in Left-Covariant Division Monoid: $a^{-1} \leq 1 \leftrightarrow 1 \leq a$

Informal description

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

Left.one_le_inv_iff theorem

: 1 ≤ a⁻¹ ↔ a ≤ 1

Full source

/-- Uses `left` co(ntra)variant. -/
@[to_additive (attr := simp) "Uses `left` co(ntra)variant."]
theorem Left.one_le_inv_iff : 1 ≤ a⁻¹ ↔ a ≤ 1 := by
  rw [← mul_le_mul_iff_left a]
  simp

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

Informal description

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

le_inv_mul_iff_mul_le theorem

: b ≤ a⁻¹ * c ↔ a * b ≤ c

Full source

@[to_additive (attr := simp)]
theorem le_inv_mul_iff_mul_le : b ≤ a⁻¹ * c ↔ a * b ≤ c := by
  rw [← mul_le_mul_iff_left a]
  simp

Inequality Equivalence: $b \leq a^{-1}c \leftrightarrow ab \leq c$ in Division Monoids

Informal description

For elements $a$, $b$, and $c$ in a division monoid, the inequality $b \leq a^{-1} * c$ holds if and only if $a * b \leq c$.

inv_mul_le_iff_le_mul theorem

: b⁻¹ * a ≤ c ↔ a ≤ b * c

Full source

@[to_additive (attr := simp)]
theorem inv_mul_le_iff_le_mul : b⁻¹b⁻¹ * a ≤ c ↔ a ≤ b * c := by
  rw [← mul_le_mul_iff_left b, mul_inv_cancel_left]

Inverse-Multiplication Inequality: $b^{-1} * a \leq c \leftrightarrow a \leq b * c$

Informal description

For elements $a, b, c$ in a division monoid, the inequality $b^{-1} * a \leq c$ holds if and only if $a \leq b * c$.

inv_le_iff_one_le_mul' theorem

: a⁻¹ ≤ b ↔ 1 ≤ a * b

Full source

@[to_additive neg_le_iff_add_nonneg']
theorem inv_le_iff_one_le_mul' : a⁻¹a⁻¹ ≤ b ↔ 1 ≤ a * b :=
  (mul_le_mul_iff_left a).symm.trans <| by rw [mul_inv_cancel]

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

Informal description

For elements $a$ and $b$ in a division monoid, the inequality $a^{-1} \leq b$ holds if and only if $1 \leq a \cdot b$.

le_inv_iff_mul_le_one_left theorem

: a ≤ b⁻¹ ↔ b * a ≤ 1

Full source

@[to_additive]
theorem le_inv_iff_mul_le_one_left : a ≤ b⁻¹ ↔ b * a ≤ 1 :=
  (mul_le_mul_iff_left b).symm.trans <| by rw [mul_inv_cancel]

Inequality Relating Element and Inverse: $a \leq b^{-1} \leftrightarrow b \cdot a \leq 1$

Informal description

For elements $a$ and $b$ in a division monoid, $a$ is less than or equal to the inverse of $b$ if and only if the product $b \cdot a$ is less than or equal to the identity element $1$.

le_inv_mul_iff_le theorem

: 1 ≤ b⁻¹ * a ↔ b ≤ a

Full source

@[to_additive]
theorem le_inv_mul_iff_le : 1 ≤ b⁻¹ * a ↔ b ≤ a := by
  rw [← mul_le_mul_iff_left b, mul_one, mul_inv_cancel_left]

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

Informal description

For elements $a$ and $b$ in a division monoid, the inequality $1 \leq b^{-1} * a$ holds if and only if $b \leq a$.

inv_mul_le_one_iff theorem

: a⁻¹ * b ≤ 1 ↔ b ≤ a

Full source

@[to_additive]
theorem inv_mul_le_one_iff : a⁻¹a⁻¹ * b ≤ 1 ↔ b ≤ a :=
  inv_mul_le_iff_le_mul.trans <| by rw [mul_one]

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

Informal description

For elements $a$ and $b$ in a division monoid, the inequality $a^{-1} * b \leq 1$ holds if and only if $b \leq a$.

Left.one_lt_inv_iff theorem

: 1 < a⁻¹ ↔ a < 1

Full source

/-- Uses `left` co(ntra)variant. -/
@[to_additive (attr := simp) Left.neg_pos_iff "Uses `left` co(ntra)variant."]
theorem Left.one_lt_inv_iff : 1 < a⁻¹ ↔ a < 1 := by
  rw [← mul_lt_mul_iff_left a, mul_inv_cancel, mul_one]

Inverse Greater Than One iff Element Less Than One (Left Variant)

Informal description

For an element $a$ in an ordered group, the inverse $a^{-1}$ is greater than the identity element $1$ if and only if $a$ is less than $1$.

Left.inv_lt_one_iff theorem

: a⁻¹ < 1 ↔ 1 < a

Full source

/-- Uses `left` co(ntra)variant. -/
@[to_additive (attr := simp) "Uses `left` co(ntra)variant."]
theorem Left.inv_lt_one_iff : a⁻¹a⁻¹ < 1 ↔ 1 < a := by
  rw [← mul_lt_mul_iff_left a, mul_inv_cancel, mul_one]

Inverse Less Than One iff One Less Than Element in Division Monoid

Informal description

For any element $a$ in a division monoid, the inverse $a^{-1}$ is less than the multiplicative identity $1$ if and only if $1$ is less than $a$.

lt_inv_mul_iff_mul_lt theorem

: b < a⁻¹ * c ↔ a * b < c

Full source

@[to_additive (attr := simp)]
theorem lt_inv_mul_iff_mul_lt : b < a⁻¹ * c ↔ a * b < c := by
  rw [← mul_lt_mul_iff_left a]
  simp

Inequality equivalence: $b < a^{-1}c \leftrightarrow ab < c$

Informal description

For elements $a$, $b$, and $c$ in a division monoid, the inequality $b < a^{-1} * c$ holds if and only if $a * b < c$.

inv_mul_lt_iff_lt_mul theorem

: b⁻¹ * a < c ↔ a < b * c

Full source

@[to_additive (attr := simp)]
theorem inv_mul_lt_iff_lt_mul : b⁻¹b⁻¹ * a < c ↔ a < b * c := by
  rw [← mul_lt_mul_iff_left b, mul_inv_cancel_left]

Inverse-Multiplication Inequality: $b^{-1} * a < c \leftrightarrow a < b * c$

Informal description

For elements $a$, $b$, and $c$ in a division monoid, the inequality $b^{-1} * a < c$ holds if and only if $a < b * c$.

inv_lt_iff_one_lt_mul' theorem

: a⁻¹ < b ↔ 1 < a * b

Full source

@[to_additive]
theorem inv_lt_iff_one_lt_mul' : a⁻¹a⁻¹ < b ↔ 1 < a * b :=
  (mul_lt_mul_iff_left a).symm.trans <| by rw [mul_inv_cancel]

Inverse Less Than iff One Less Than Product

Informal description

For elements $a$ and $b$ in a division monoid, the inverse of $a$ is less than $b$ if and only if the identity element $1$ is less than the product $a \cdot b$. That is, $a^{-1} < b \leftrightarrow 1 < a \cdot b$.

lt_inv_iff_mul_lt_one' theorem

: a < b⁻¹ ↔ b * a < 1

Full source

@[to_additive]
theorem lt_inv_iff_mul_lt_one' : a < b⁻¹ ↔ b * a < 1 :=
  (mul_lt_mul_iff_left b).symm.trans <| by rw [mul_inv_cancel]

Inequality between element and inverse: $a < b^{-1} \leftrightarrow b \cdot a < 1$

Informal description

For elements $a$ and $b$ in a division monoid, $a$ is less than the inverse of $b$ if and only if the product $b \cdot a$ is less than the multiplicative identity $1$.

lt_inv_mul_iff_lt theorem

: 1 < b⁻¹ * a ↔ b < a

Full source

@[to_additive]
theorem lt_inv_mul_iff_lt : 1 < b⁻¹ * a ↔ b < a := by
  rw [← mul_lt_mul_iff_left b, mul_one, mul_inv_cancel_left]

Inequality equivalence: $1 < b^{-1}a \leftrightarrow b < a$

Informal description

For elements $a$ and $b$ in a division monoid, the inequality $1 < b^{-1} * a$ holds if and only if $b < a$.

inv_mul_lt_one_iff theorem

: a⁻¹ * b < 1 ↔ b < a

Full source

@[to_additive]
theorem inv_mul_lt_one_iff : a⁻¹a⁻¹ * b < 1 ↔ b < a :=
  _root_.trans inv_mul_lt_iff_lt_mul <| by rw [mul_one]

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

Informal description

For elements $a$ and $b$ in a division monoid, the inequality $a^{-1} * b < 1$ holds if and only if $b < a$.

Right.inv_le_one_iff theorem

: a⁻¹ ≤ 1 ↔ 1 ≤ a

Full source

/-- Uses `right` co(ntra)variant. -/
@[to_additive (attr := simp) "Uses `right` co(ntra)variant."]
theorem Right.inv_le_one_iff : a⁻¹a⁻¹ ≤ 1 ↔ 1 ≤ a := by
  rw [← mul_le_mul_iff_right a]
  simp

Inverse Inequality: $a^{-1} \leq 1 \leftrightarrow 1 \leq a$ in Division Monoids

Informal description

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

Right.one_le_inv_iff theorem

: 1 ≤ a⁻¹ ↔ a ≤ 1

Full source

/-- Uses `right` co(ntra)variant. -/
@[to_additive (attr := simp) "Uses `right` co(ntra)variant."]
theorem Right.one_le_inv_iff : 1 ≤ a⁻¹ ↔ a ≤ 1 := by
  rw [← mul_le_mul_iff_right a]
  simp

Right Inverse Inequality: $1 \leq a^{-1} \leftrightarrow a \leq 1$

Informal description

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

inv_le_iff_one_le_mul theorem

: a⁻¹ ≤ b ↔ 1 ≤ b * a

Full source

@[to_additive neg_le_iff_add_nonneg]
theorem inv_le_iff_one_le_mul : a⁻¹a⁻¹ ≤ b ↔ 1 ≤ b * a :=
  (mul_le_mul_iff_right a).symm.trans <| by rw [inv_mul_cancel]

Inverse Inequality Characterization: $a^{-1} \leq b \leftrightarrow 1 \leq b \cdot a$

Informal description

For elements $a$ and $b$ in a division monoid, the inequality $a^{-1} \leq b$ holds if and only if $1 \leq b \cdot a$.

le_inv_iff_mul_le_one_right theorem

: a ≤ b⁻¹ ↔ a * b ≤ 1

Full source

@[to_additive]
theorem le_inv_iff_mul_le_one_right : a ≤ b⁻¹ ↔ a * b ≤ 1 :=
  (mul_le_mul_iff_right b).symm.trans <| by rw [inv_mul_cancel]

Inequality Relating Element to Inverse via Product with Identity

Informal description

For elements $a$ and $b$ in a division monoid, $a$ is less than or equal to the inverse of $b$ if and only if the product $a * b$ is less than or equal to the multiplicative identity $1$.

mul_inv_le_iff_le_mul theorem

: a * b⁻¹ ≤ c ↔ a ≤ c * b

Full source

@[to_additive (attr := simp)]
theorem mul_inv_le_iff_le_mul : a * b⁻¹ ≤ c ↔ a ≤ c * b :=
  (mul_le_mul_iff_right b).symm.trans <| by rw [inv_mul_cancel_right]

Inequality equivalence: $a \cdot b^{-1} \leq c \leftrightarrow a \leq c \cdot b$

Informal description

For elements $a$, $b$, and $c$ in a division monoid, the inequality $a \cdot b^{-1} \leq c$ holds if and only if $a \leq c \cdot b$.

le_mul_inv_iff_mul_le theorem

: c ≤ a * b⁻¹ ↔ c * b ≤ a

Full source

@[to_additive (attr := simp)]
theorem le_mul_inv_iff_mul_le : c ≤ a * b⁻¹ ↔ c * b ≤ a :=
  (mul_le_mul_iff_right b).symm.trans <| by rw [inv_mul_cancel_right]

Inequality Equivalence: $c \leq a b^{-1} \leftrightarrow c b \leq a$ in Division Monoids

Informal description

For elements $a$, $b$, and $c$ in a division monoid, the inequality $c \leq a \cdot b^{-1}$ holds if and only if $c \cdot b \leq a$ holds.

mul_inv_le_one_iff_le theorem

: a * b⁻¹ ≤ 1 ↔ a ≤ b

Full source

@[to_additive]
theorem mul_inv_le_one_iff_le : a * b⁻¹ ≤ 1 ↔ a ≤ b :=
  mul_inv_le_iff_le_mul.trans <| by rw [one_mul]

Inequality Characterization via Right Division: $a \cdot b^{-1} \leq 1 \leftrightarrow a \leq b$

Informal description

For elements $a$ and $b$ in a division monoid, the inequality $a \cdot b^{-1} \leq 1$ holds if and only if $a \leq b$.

le_mul_inv_iff_le theorem

: 1 ≤ a * b⁻¹ ↔ b ≤ a

Full source

@[to_additive]
theorem le_mul_inv_iff_le : 1 ≤ a * b⁻¹ ↔ b ≤ a := by
  rw [← mul_le_mul_iff_right b, one_mul, inv_mul_cancel_right]

Inequality Characterization via Right Division: $1 \leq a \cdot b^{-1} \leftrightarrow b \leq a$

Informal description

For elements $a$ and $b$ in a division monoid, the inequality $1 \leq a \cdot b^{-1}$ holds if and only if $b \leq a$.

mul_inv_le_one_iff theorem

: b * a⁻¹ ≤ 1 ↔ b ≤ a

Full source

@[to_additive]
theorem mul_inv_le_one_iff : b * a⁻¹ ≤ 1 ↔ b ≤ a :=
  _root_.trans mul_inv_le_iff_le_mul <| by rw [one_mul]

Inequality Characterization via Left Division: $b \cdot a^{-1} \leq 1 \leftrightarrow b \leq a$

Informal description

For elements $a$ and $b$ in a division monoid, the inequality $b \cdot a^{-1} \leq 1$ holds if and only if $b \leq a$.

Right.inv_lt_one_iff theorem

: a⁻¹ < 1 ↔ 1 < a

Full source

/-- Uses `right` co(ntra)variant. -/
@[to_additive (attr := simp) "Uses `right` co(ntra)variant."]
theorem Right.inv_lt_one_iff : a⁻¹a⁻¹ < 1 ↔ 1 < a := by
  rw [← mul_lt_mul_iff_right a, inv_mul_cancel, one_mul]

Inverse Less Than One iff One Less Than Element in Division Monoid

Informal description

For any element $a$ in a division monoid, the inverse $a^{-1}$ is less than $1$ if and only if $1$ is less than $a$.

Right.one_lt_inv_iff theorem

: 1 < a⁻¹ ↔ a < 1

Full source

/-- Uses `right` co(ntra)variant. -/
@[to_additive (attr := simp) Right.neg_pos_iff "Uses `right` co(ntra)variant."]
theorem Right.one_lt_inv_iff : 1 < a⁻¹ ↔ a < 1 := by
  rw [← mul_lt_mul_iff_right a, inv_mul_cancel, one_mul]

Inverse Greater Than One iff Element Less Than One

Informal description

For an element $a$ in a division monoid, the inverse $a^{-1}$ is greater than $1$ if and only if $a$ is less than $1$.

inv_lt_iff_one_lt_mul theorem

: a⁻¹ < b ↔ 1 < b * a

Full source

@[to_additive]
theorem inv_lt_iff_one_lt_mul : a⁻¹a⁻¹ < b ↔ 1 < b * a :=
  (mul_lt_mul_iff_right a).symm.trans <| by rw [inv_mul_cancel]

Inverse Inequality: $a^{-1} < b \leftrightarrow 1 < b \cdot a$

Informal description

For elements $a$ and $b$ in a division monoid, the inverse of $a$ is less than $b$ if and only if $1$ is less than the product $b \cdot a$. That is, $a^{-1} < b \leftrightarrow 1 < b \cdot a$.

lt_inv_iff_mul_lt_one theorem

: a < b⁻¹ ↔ a * b < 1

Full source

@[to_additive]
theorem lt_inv_iff_mul_lt_one : a < b⁻¹ ↔ a * b < 1 :=
  (mul_lt_mul_iff_right b).symm.trans <| by rw [inv_mul_cancel]

Inequality between element and inverse: $a < b^{-1} \leftrightarrow a * b < 1$

Informal description

For elements $a$ and $b$ in a division monoid, $a$ is less than the inverse of $b$ if and only if the product $a * b$ is less than $1$.

mul_inv_lt_iff_lt_mul theorem

: a * b⁻¹ < c ↔ a < c * b

Full source

@[to_additive (attr := simp)]
theorem mul_inv_lt_iff_lt_mul : a * b⁻¹ < c ↔ a < c * b := by
  rw [← mul_lt_mul_iff_right b, inv_mul_cancel_right]

Inequality equivalence: $a \cdot b^{-1} < c \leftrightarrow a < c \cdot b$

Informal description

For elements $a$, $b$, and $c$ in a division monoid, the inequality $a \cdot b^{-1} < c$ holds if and only if $a < c \cdot b$ holds.

lt_mul_inv_iff_mul_lt theorem

: c < a * b⁻¹ ↔ c * b < a

Full source

@[to_additive (attr := simp)]
theorem lt_mul_inv_iff_mul_lt : c < a * b⁻¹ ↔ c * b < a :=
  (mul_lt_mul_iff_right b).symm.trans <| by rw [inv_mul_cancel_right]

Inequality equivalence: $c < a b^{-1} \leftrightarrow c b < a$

Informal description

For elements $a, b, c$ in a division monoid, the inequality $c < a \cdot b^{-1}$ holds if and only if $c \cdot b < a$ holds.

inv_mul_lt_one_iff_lt theorem

: a * b⁻¹ < 1 ↔ a < b

Full source

@[to_additive]
theorem inv_mul_lt_one_iff_lt : a * b⁻¹ < 1 ↔ a < b := by
  rw [← mul_lt_mul_iff_right b, inv_mul_cancel_right, one_mul]

Inverse-Multiplication Inequality: $a \cdot b^{-1} < 1 \leftrightarrow a < b$

Informal description

For elements $a$ and $b$ in a division monoid, the inequality $a \cdot b^{-1} < 1$ holds if and only if $a < b$.

lt_mul_inv_iff_lt theorem

: 1 < a * b⁻¹ ↔ b < a

Full source

@[to_additive]
theorem lt_mul_inv_iff_lt : 1 < a * b⁻¹ ↔ b < a := by
  rw [← mul_lt_mul_iff_right b, one_mul, inv_mul_cancel_right]

Inequality Characterization via Right Multiplication by Inverse: $1 < a b^{-1} \leftrightarrow b < a$

Informal description

For elements $a$ and $b$ in a division monoid $\alpha$, the inequality $1 < a \cdot b^{-1}$ holds if and only if $b < a$.

mul_inv_lt_one_iff theorem

: b * a⁻¹ < 1 ↔ b < a

Full source

@[to_additive]
theorem mul_inv_lt_one_iff : b * a⁻¹ < 1 ↔ b < a :=
  _root_.trans mul_inv_lt_iff_lt_mul <| by rw [one_mul]

Inequality Characterization via Left Multiplication by Inverse: $b \cdot a^{-1} < 1 \leftrightarrow b < a$

Informal description

For elements $a$ and $b$ in a division monoid, the inequality $b \cdot a^{-1} < 1$ holds if and only if $b < a$.

div_le_self_iff theorem

(a : α) {b : α} : a / b ≤ a ↔ 1 ≤ b

Full source

@[to_additive (attr := simp)]
theorem div_le_self_iff (a : α) {b : α} : a / b ≤ a ↔ 1 ≤ b := by
  simp [div_eq_mul_inv]

Division Inequality: $a / b \leq a \leftrightarrow 1 \leq b$

Informal description

For any elements $a$ and $b$ in a division monoid $\alpha$, the inequality $a / b \leq a$ holds if and only if $1 \leq b$.

le_div_self_iff theorem

(a : α) {b : α} : a ≤ a / b ↔ b ≤ 1

Full source

@[to_additive (attr := simp)]
theorem le_div_self_iff (a : α) {b : α} : a ≤ a / b ↔ b ≤ 1 := by
  simp [div_eq_mul_inv]

Inequality Characterizing Division by Elements Less Than or Equal to One

Informal description

For any elements $a$ and $b$ in a division monoid $\alpha$, the inequality $a \leq a / b$ holds if and only if $b \leq 1$.

inv_le_inv_iff theorem

: a⁻¹ ≤ b⁻¹ ↔ b ≤ a

Full source

@[to_additive (attr := simp)]
theorem inv_le_inv_iff : a⁻¹a⁻¹ ≤ b⁻¹ ↔ b ≤ a := by
  rw [← mul_le_mul_iff_left a, ← mul_le_mul_iff_right b]
  simp

Inverse Inequality Equivalence: $a^{-1} \leq b^{-1} \leftrightarrow b \leq a$

Informal description

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

mul_inv_le_inv_mul_iff theorem

: a * b⁻¹ ≤ d⁻¹ * c ↔ d * a ≤ c * b

Full source

@[to_additive]
theorem mul_inv_le_inv_mul_iff : a * b⁻¹ ≤ d⁻¹ * c ↔ d * a ≤ c * b := by
  rw [← mul_le_mul_iff_left d, ← mul_le_mul_iff_right b, mul_inv_cancel_left, mul_assoc,
    inv_mul_cancel_right]

Inequality Equivalence: $a b^{-1} \leq d^{-1} c \leftrightarrow d a \leq c b$

Informal description

For elements $a, b, c, d$ in a division monoid $\alpha$, the inequality $a * b^{-1} \leq d^{-1} * c$ holds if and only if $d * a \leq c * b$.

div_lt_self_iff theorem

(a : α) {b : α} : a / b < a ↔ 1 < b

Full source

@[to_additive (attr := simp)]
theorem div_lt_self_iff (a : α) {b : α} : a / b < a ↔ 1 < b := by
  simp [div_eq_mul_inv]

Inequality $a / b < a$ iff $1 < b$ in a division monoid

Informal description

For any elements $a$ and $b$ in a division monoid $\alpha$, the inequality $a / b < a$ holds if and only if $1 < b$.

inv_lt_inv_iff theorem

: a⁻¹ < b⁻¹ ↔ b < a

Full source

@[to_additive (attr := simp)]
theorem inv_lt_inv_iff : a⁻¹a⁻¹ < b⁻¹ ↔ b < a := by
  rw [← mul_lt_mul_iff_left a, ← mul_lt_mul_iff_right b]
  simp

Inverse Inequality: $a^{-1} < b^{-1} \leftrightarrow b < a$

Informal description

For any elements $a$ and $b$ in an ordered group, the inequality $a^{-1} < b^{-1}$ holds if and only if $b < a$.

inv_lt' theorem

: a⁻¹ < b ↔ b⁻¹ < a

Full source

@[to_additive neg_lt]
theorem inv_lt' : a⁻¹a⁻¹ < b ↔ b⁻¹ < a := by rw [← inv_lt_inv_iff, inv_inv]

Inverse Inequality: $a^{-1} < b \leftrightarrow b^{-1} < a$

Informal description

For any elements $a$ and $b$ in an ordered group, the inequality $a^{-1} < b$ holds if and only if $b^{-1} < a$.

lt_inv' theorem

: a < b⁻¹ ↔ b < a⁻¹

Full source

@[to_additive lt_neg]
theorem lt_inv' : a < b⁻¹ ↔ b < a⁻¹ := by rw [← inv_lt_inv_iff, inv_inv]

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

Informal description

For any elements $a$ and $b$ in an ordered group, the inequality $a < b^{-1}$ holds if and only if $b < a^{-1}$.

mul_inv_lt_inv_mul_iff theorem

: a * b⁻¹ < d⁻¹ * c ↔ d * a < c * b

Full source

@[to_additive]
theorem mul_inv_lt_inv_mul_iff : a * b⁻¹ < d⁻¹ * c ↔ d * a < c * b := by
  rw [← mul_lt_mul_iff_left d, ← mul_lt_mul_iff_right b, mul_inv_cancel_left, mul_assoc,
    inv_mul_cancel_right]

Inequality equivalence: $a b^{-1} < d^{-1} c \leftrightarrow d a < c b$ in a division monoid

Informal description

For elements $a, b, c, d$ in a division monoid, the inequality $a * b^{-1} < d^{-1} * c$ holds if and only if $d * a < c * b$.

Left.inv_le_self theorem

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

Full source

@[to_additive]
theorem Left.inv_le_self (h : 1 ≤ a) : a⁻¹ ≤ a :=
  le_trans (Left.inv_le_one_iff.mpr h) h

Inverse Inequality in Left-Covariant Division Monoid: $1 \leq a \Rightarrow a^{-1} \leq a$

Informal description

For any element $a$ in a left-covariant division monoid, if $1 \leq a$, then the inverse $a^{-1}$ is less than or equal to $a$.

Left.self_le_inv theorem

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

Full source

@[to_additive]
theorem Left.self_le_inv (h : a ≤ 1) : a ≤ a⁻¹ :=
  le_trans h (Left.one_le_inv_iff.mpr h)

Element Less Than or Equal to One Implies $a \leq a^{-1}$

Informal description

For any element $a$ in a division monoid, if $a \leq 1$, then $a \leq a^{-1}$.

Left.inv_lt_self theorem

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

Full source

@[to_additive]
theorem Left.inv_lt_self (h : 1 < a) : a⁻¹ < a :=
  (Left.inv_lt_one_iff.mpr h).trans h

Inverse is Less Than Element When Greater Than One

Informal description

For any element $a$ in a division monoid, if $1 < a$, then the inverse $a^{-1}$ is strictly less than $a$.

Left.self_lt_inv theorem

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

Full source

@[to_additive]
theorem Left.self_lt_inv (h : a < 1) : a < a⁻¹ :=
  lt_trans h (Left.one_lt_inv_iff.mpr h)

Element is Less Than Its Inverse When Less Than One (Left Variant)

Informal description

For any element $a$ in a division monoid, if $a < 1$, then $a < a^{-1}$.

Right.inv_le_self theorem

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

Full source

@[to_additive]
theorem Right.inv_le_self (h : 1 ≤ a) : a⁻¹ ≤ a :=
  le_trans (Right.inv_le_one_iff.mpr h) h

Inverse is Less Than or Equal to Element When One is Less Than or Equal to Element in Division Monoid

Informal description

For any element $a$ in a division monoid, if $1 \leq a$, then the inverse $a^{-1}$ is less than or equal to $a$.

Right.self_le_inv theorem

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

Full source

@[to_additive]
theorem Right.self_le_inv (h : a ≤ 1) : a ≤ a⁻¹ :=
  le_trans h (Right.one_le_inv_iff.mpr h)

Element is Less Than or Equal to Its Inverse When Less Than or Equal to One

Informal description

For any element $a$ in a division monoid, if $a \leq 1$, then $a \leq a^{-1}$.

Right.inv_lt_self theorem

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

Full source

@[to_additive]
theorem Right.inv_lt_self (h : 1 < a) : a⁻¹ < a :=
  (Right.inv_lt_one_iff.mpr h).trans h

Inverse is Less Than Element When One is Less Than Element in Division Monoid

Informal description

For any element $a$ in a division monoid, if $1 < a$, then the inverse $a^{-1}$ is strictly less than $a$.

Right.self_lt_inv theorem

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

Full source

@[to_additive]
theorem Right.self_lt_inv (h : a < 1) : a < a⁻¹ :=
  lt_trans h (Right.one_lt_inv_iff.mpr h)

Element is Less Than Its Inverse When Less Than One

Informal description

For any element $a$ in a division monoid, if $a < 1$, then $a < a^{-1}$.

inv_mul_le_iff_le_mul' theorem

: c⁻¹ * a ≤ b ↔ a ≤ b * c

Full source

@[to_additive]
theorem inv_mul_le_iff_le_mul' : c⁻¹c⁻¹ * a ≤ b ↔ a ≤ b * c := by rw [inv_mul_le_iff_le_mul, mul_comm]

Inverse-Multiplication Inequality (Variant): $c^{-1} * a \leq b \leftrightarrow a \leq b * c$

Informal description

For elements $a, b, c$ in a division monoid, the inequality $c^{-1} * a \leq b$ holds if and only if $a \leq b * c$.

mul_inv_le_iff_le_mul' theorem

: a * b⁻¹ ≤ c ↔ a ≤ b * c

Full source

@[to_additive]
theorem mul_inv_le_iff_le_mul' : a * b⁻¹ ≤ c ↔ a ≤ b * c := by
  rw [← inv_mul_le_iff_le_mul, mul_comm]

Multiplication-Inversion Inequality: $a \cdot b^{-1} \leq c \leftrightarrow a \leq b \cdot c$

Informal description

For elements $a, b, c$ in a division monoid, the inequality $a \cdot b^{-1} \leq c$ holds if and only if $a \leq b \cdot c$.

mul_inv_le_mul_inv_iff' theorem

: a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b

Full source

@[to_additive add_neg_le_add_neg_iff]
theorem mul_inv_le_mul_inv_iff' : a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b := by
  rw [mul_comm c, mul_inv_le_inv_mul_iff, mul_comm]

Inequality Equivalence: $a b^{-1} \leq c d^{-1} \leftrightarrow a d \leq c b$

Informal description

For elements $a, b, c, d$ in a division monoid, the inequality $a \cdot b^{-1} \leq c \cdot d^{-1}$ holds if and only if $a \cdot d \leq c \cdot b$.

inv_mul_lt_iff_lt_mul' theorem

: c⁻¹ * a < b ↔ a < b * c

Full source

@[to_additive]
theorem inv_mul_lt_iff_lt_mul' : c⁻¹c⁻¹ * a < b ↔ a < b * c := by rw [inv_mul_lt_iff_lt_mul, mul_comm]

Inequality equivalence: $c^{-1} * a < b \leftrightarrow a < b * c$ in a division monoid

Informal description

For elements $a$, $b$, and $c$ in a division monoid, the inequality $c^{-1} * a < b$ holds if and only if $a < b * c$.

mul_inv_lt_iff_le_mul' theorem

: a * b⁻¹ < c ↔ a < b * c

Full source

@[to_additive]
theorem mul_inv_lt_iff_le_mul' : a * b⁻¹ < c ↔ a < b * c := by
  rw [← inv_mul_lt_iff_lt_mul, mul_comm]

Inequality equivalence: $a b^{-1} < c \leftrightarrow a < b c$ in a division monoid

Informal description

For elements $a$, $b$, and $c$ in a division monoid, the inequality $a * b^{-1} < c$ holds if and only if $a < b * c$.

mul_inv_lt_mul_inv_iff' theorem

: a * b⁻¹ < c * d⁻¹ ↔ a * d < c * b

Full source

@[to_additive add_neg_lt_add_neg_iff]
theorem mul_inv_lt_mul_inv_iff' : a * b⁻¹ < c * d⁻¹ ↔ a * d < c * b := by
  rw [mul_comm c, mul_inv_lt_inv_mul_iff, mul_comm]

Inequality equivalence: $a b^{-1} < c d^{-1} \leftrightarrow a d < c b$ in a division monoid

Informal description

For elements $a, b, c, d$ in a division monoid, the inequality $a * b^{-1} < c * d^{-1}$ holds if and only if $a * d < c * b$.

div_le_div_iff_right theorem

(c : α) : a / c ≤ b / c ↔ a ≤ b

Full source

@[to_additive]
theorem div_le_div_iff_right (c : α) : a / c ≤ b / c ↔ a ≤ b := by
  simpa only [div_eq_mul_inv] using mul_le_mul_iff_right _

Division Preserves Order in Ordered Groups

Informal description

For any elements $a, b, c$ in an ordered group $\alpha$, the inequality $a / c \leq b / c$ holds if and only if $a \leq b$.

div_le_div_right' theorem

(h : a ≤ b) (c : α) : a / c ≤ b / c

Full source

@[to_additive (attr := gcongr) sub_le_sub_right]
theorem div_le_div_right' (h : a ≤ b) (c : α) : a / c ≤ b / c :=
  (div_le_div_iff_right c).2 h

Right Division Preserves Order in Ordered Groups

Informal description

For any elements $a, b, c$ in an ordered group $\alpha$, if $a \leq b$, then $a / c \leq b / c$.

one_le_div' theorem

: 1 ≤ a / b ↔ b ≤ a

Full source

@[to_additive (attr := simp) sub_nonneg]
theorem one_le_div' : 1 ≤ a / b ↔ b ≤ a := by
  rw [← mul_le_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]

Inequality Equivalence: $1 \leq a / b \leftrightarrow b \leq a$ in Ordered Groups

Informal description

For any elements $a, b$ in an ordered group, the inequality $1 \leq a / b$ holds if and only if $b \leq a$.

div_le_one' theorem

: a / b ≤ 1 ↔ a ≤ b

Full source

@[to_additive sub_nonpos]
theorem div_le_one' : a / b ≤ 1 ↔ a ≤ b := by
  rw [← mul_le_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]

Division Inequality: $a / b \leq 1 \leftrightarrow a \leq b$

Informal description

For elements $a$ and $b$ in an ordered group, the inequality $a / b \leq 1$ holds if and only if $a \leq b$.

le_div_iff_mul_le theorem

: a ≤ c / b ↔ a * b ≤ c

Full source

@[to_additive]
theorem le_div_iff_mul_le : a ≤ c / b ↔ a * b ≤ c := by
  rw [← mul_le_mul_iff_right b, div_eq_mul_inv, inv_mul_cancel_right]

Inequality Equivalence: $a \leq c / b \leftrightarrow a \cdot b \leq c$ in Ordered Groups

Informal description

For elements $a$, $b$, and $c$ in an ordered group, the inequality $a \leq c / b$ holds if and only if $a \cdot b \leq c$ holds.

div_le_iff_le_mul theorem

: a / c ≤ b ↔ a ≤ b * c

Full source

@[to_additive]
theorem div_le_iff_le_mul : a / c ≤ b ↔ a ≤ b * c := by
  rw [← mul_le_mul_iff_right c, div_eq_mul_inv, inv_mul_cancel_right]

Division Inequality: $a / c \leq b \leftrightarrow a \leq b \cdot c$

Informal description

For elements $a$, $b$, and $c$ in an ordered group, the inequality $a / c \leq b$ holds if and only if $a \leq b \cdot c$.

AddGroup.toOrderedSub instance

{α : Type*} [AddGroup α] [LE α] [AddRightMono α] : OrderedSub α

Full source

instance (priority := 100) AddGroup.toOrderedSub {α : Type*} [AddGroup α] [LE α]
    [AddRightMono α] : OrderedSub α :=
  ⟨fun _ _ _ => sub_le_iff_le_add⟩

Ordered Subtraction in Additive Groups with Right-Monotone Addition

Informal description

For any additive group $\alpha$ with a partial order and right-monotone addition, $\alpha$ has an ordered subtraction structure.

div_le_div_iff_left theorem

(a : α) : a / b ≤ a / c ↔ c ≤ b

Full source

@[to_additive]
theorem div_le_div_iff_left (a : α) : a / b ≤ a / c ↔ c ≤ b := by
  rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_le_mul_iff_left a⁻¹, inv_mul_cancel_left,
    inv_mul_cancel_left, inv_le_inv_iff]

Division Inequality Comparison: $a / b \leq a / c \leftrightarrow c \leq b$

Informal description

For any elements $a$, $b$, and $c$ in a division monoid $\alpha$, the inequality $a / b \leq a / c$ holds if and only if $c \leq b$.

div_le_div_left' theorem

(h : a ≤ b) (c : α) : c / b ≤ c / a

Full source

@[to_additive (attr := gcongr) sub_le_sub_left]
theorem div_le_div_left' (h : a ≤ b) (c : α) : c / b ≤ c / a :=
  (div_le_div_iff_left c).2 h

Division Inequality: $a \leq b$ implies $c / b \leq c / a$

Informal description

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

div_le_div_iff' theorem

: a / b ≤ c / d ↔ a * d ≤ c * b

Full source

/-- See also `div_le_div_iff` for a version that works for `LinearOrderedSemifield` with
additional assumptions. -/
@[to_additive sub_le_sub_iff]
theorem div_le_div_iff' : a / b ≤ c / d ↔ a * d ≤ c * b := by
  simpa only [div_eq_mul_inv] using mul_inv_le_mul_inv_iff'

Inequality Equivalence: $\frac{a}{b} \leq \frac{c}{d} \leftrightarrow a d \leq c b$

Informal description

For elements $a, b, c, d$ in an ordered group, the inequality $\frac{a}{b} \leq \frac{c}{d}$ holds if and only if $a \cdot d \leq c \cdot b$.

le_div_iff_mul_le' theorem

: b ≤ c / a ↔ a * b ≤ c

Full source

@[to_additive]
theorem le_div_iff_mul_le' : b ≤ c / a ↔ a * b ≤ c := by rw [le_div_iff_mul_le, mul_comm]

Inequality Equivalence: $b \leq c / a \leftrightarrow a \cdot b \leq c$ in Ordered Groups

Informal description

For elements $a$, $b$, and $c$ in an ordered group, the inequality $b \leq c / a$ holds if and only if $a \cdot b \leq c$ holds.

div_le_iff_le_mul' theorem

: a / b ≤ c ↔ a ≤ b * c

Full source

@[to_additive]
theorem div_le_iff_le_mul' : a / b ≤ c ↔ a ≤ b * c := by rw [div_le_iff_le_mul, mul_comm]

Division Inequality: $a / b \leq c \leftrightarrow a \leq b \cdot c$

Informal description

For elements $a$, $b$, and $c$ in an ordered group, the inequality $a / b \leq c$ holds if and only if $a \leq b \cdot c$.

inv_le_div_iff_le_mul theorem

: b⁻¹ ≤ a / c ↔ c ≤ a * b

Full source

@[to_additive (attr := simp)]
theorem inv_le_div_iff_le_mul : b⁻¹b⁻¹ ≤ a / c ↔ c ≤ a * b :=
  le_div_iff_mul_le.trans inv_mul_le_iff_le_mul'

Inverse Inequality Equivalence: $b^{-1} \leq a/c \leftrightarrow c \leq a \cdot b$

Informal description

For elements $a, b, c$ in an ordered group, the inequality $b^{-1} \leq a / c$ holds if and only if $c \leq a \cdot b$.

inv_le_div_iff_le_mul' theorem

: a⁻¹ ≤ b / c ↔ c ≤ a * b

Full source

@[to_additive]
theorem inv_le_div_iff_le_mul' : a⁻¹a⁻¹ ≤ b / c ↔ c ≤ a * b := by rw [inv_le_div_iff_le_mul, mul_comm]

Inverse Inequality Equivalence: $a^{-1} \leq b/c \leftrightarrow c \leq a \cdot b$

Informal description

For any elements $a$, $b$, and $c$ in an ordered group, the inequality $a^{-1} \leq b / c$ holds if and only if $c \leq a \cdot b$.

div_le_comm theorem

: a / b ≤ c ↔ a / c ≤ b

Full source

@[to_additive]
theorem div_le_comm : a / b ≤ c ↔ a / c ≤ b :=
  div_le_iff_le_mul'.trans div_le_iff_le_mul.symm

Division Inequality Equivalence: $a/b \leq c \leftrightarrow a/c \leq b$

Informal description

For any elements $a$, $b$, and $c$ in an ordered group, the inequality $a / b \leq c$ holds if and only if $a / c \leq b$ holds.

le_div_comm theorem

: a ≤ b / c ↔ c ≤ b / a

Full source

@[to_additive]
theorem le_div_comm : a ≤ b / c ↔ c ≤ b / a :=
  le_div_iff_mul_le'.trans le_div_iff_mul_le.symm

Inequality Equivalence: $a \leq b/c \leftrightarrow c \leq b/a$ in Ordered Groups

Informal description

For any elements $a$, $b$, and $c$ in an ordered group, the inequality $a \leq b / c$ holds if and only if $c \leq b / a$ holds.

div_le_div'' theorem

(hab : a ≤ b) (hcd : c ≤ d) : a / d ≤ b / c

Full source

@[to_additive (attr := gcongr) sub_le_sub]
theorem div_le_div'' (hab : a ≤ b) (hcd : c ≤ d) : a / d ≤ b / c := by
  rw [div_eq_mul_inv, div_eq_mul_inv, mul_comm b, mul_inv_le_inv_mul_iff, mul_comm]
  exact mul_le_mul' hab hcd

Division Inequality: $a \leq b$ and $c \leq d$ implies $a/d \leq b/c$

Informal description

For any elements $a, b, c, d$ in an ordered group such that $a \leq b$ and $c \leq d$, the inequality $a / d \leq b / c$ holds.

div_lt_div_iff_right theorem

(c : α) : a / c < b / c ↔ a < b

Full source

@[to_additive (attr := simp)]
theorem div_lt_div_iff_right (c : α) : a / c < b / c ↔ a < b := by
  simpa only [div_eq_mul_inv] using mul_lt_mul_iff_right _

Division preserves strict inequality in ordered groups: $a / c < b / c \leftrightarrow a < b$

Informal description

For any elements $a$, $b$, and $c$ in an ordered group, the inequality $a / c < b / c$ holds if and only if $a < b$.

div_lt_div_right' theorem

(h : a < b) (c : α) : a / c < b / c

Full source

@[to_additive (attr := gcongr) sub_lt_sub_right]
theorem div_lt_div_right' (h : a < b) (c : α) : a / c < b / c :=
  (div_lt_div_iff_right c).2 h

Right Division Preserves Strict Inequality in Ordered Groups: $a / c < b / c$ when $a < b$

Informal description

For any elements $a$ and $b$ in an ordered group with $a < b$, and for any element $c$ in the same group, the inequality $a / c < b / c$ holds.

one_lt_div' theorem

: 1 < a / b ↔ b < a

Full source

@[to_additive (attr := simp) sub_pos]
theorem one_lt_div' : 1 < a / b ↔ b < a := by
  rw [← mul_lt_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]

Inequality equivalence: $1 < a/b \leftrightarrow b < a$

Informal description

For any elements $a$ and $b$ in an ordered group, the inequality $1 < a/b$ holds if and only if $b < a$.

div_lt_one' theorem

: a / b < 1 ↔ a < b

Full source

@[to_additive (attr := simp) sub_neg "For `a - -b = a + b`, see `sub_neg_eq_add`."]
theorem div_lt_one' : a / b < 1 ↔ a < b := by
  rw [← mul_lt_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]

Division-Unit Inequality: $a / b < 1 \leftrightarrow a < b$

Informal description

For elements $a$ and $b$ in an ordered group, the inequality $a / b < 1$ holds if and only if $a < b$.

lt_div_iff_mul_lt theorem

: a < c / b ↔ a * b < c

Full source

@[to_additive]
theorem lt_div_iff_mul_lt : a < c / b ↔ a * b < c := by
  rw [← mul_lt_mul_iff_right b, div_eq_mul_inv, inv_mul_cancel_right]

Inequality equivalence: $a < c/b \leftrightarrow a \cdot b < c$

Informal description

For elements $a$, $b$, and $c$ in an ordered group, the inequality $a < c / b$ holds if and only if $a \cdot b < c$.

div_lt_iff_lt_mul theorem

: a / c < b ↔ a < b * c

Full source

@[to_additive]
theorem div_lt_iff_lt_mul : a / c < b ↔ a < b * c := by
  rw [← mul_lt_mul_iff_right c, div_eq_mul_inv, inv_mul_cancel_right]

Division-Multiplication Inequality: $a / c < b \leftrightarrow a < b \cdot c$

Informal description

For elements $a$, $b$, and $c$ in an ordered group, the inequality $a / c < b$ holds if and only if $a < b \cdot c$.

div_lt_div_iff_left theorem

(a : α) : a / b < a / c ↔ c < b

Full source

@[to_additive (attr := simp)]
theorem div_lt_div_iff_left (a : α) : a / b < a / c ↔ c < b := by
  rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_lt_mul_iff_left a⁻¹, inv_mul_cancel_left,
    inv_mul_cancel_left, inv_lt_inv_iff]

Division Inequality: $a/b < a/c \leftrightarrow c < b$

Informal description

For any element $a$ in an ordered group, and for any elements $b$ and $c$ in the same group, the inequality $a / b < a / c$ holds if and only if $c < b$.

inv_lt_div_iff_lt_mul theorem

: a⁻¹ < b / c ↔ c < a * b

Full source

@[to_additive (attr := simp)]
theorem inv_lt_div_iff_lt_mul : a⁻¹a⁻¹ < b / c ↔ c < a * b := by
  rw [div_eq_mul_inv, lt_mul_inv_iff_mul_lt, inv_mul_lt_iff_lt_mul]

Inverse-Division Inequality: $a^{-1} < b/c \leftrightarrow c < a b$

Informal description

For elements $a$, $b$, and $c$ in a division monoid, the inequality $a^{-1} < b / c$ holds if and only if $c < a \cdot b$.

div_lt_div_left' theorem

(h : a < b) (c : α) : c / b < c / a

Full source

@[to_additive (attr := gcongr) sub_lt_sub_left]
theorem div_lt_div_left' (h : a < b) (c : α) : c / b < c / a :=
  (div_lt_div_iff_left c).2 h

Division Inequality: $c/b < c/a$ when $a < b$

Informal description

For any elements $a$ and $b$ in an ordered group such that $a < b$, and for any element $c$ in the same group, the inequality $c / b < c / a$ holds.

div_lt_div_iff' theorem

: a / b < c / d ↔ a * d < c * b

Full source

@[to_additive sub_lt_sub_iff]
theorem div_lt_div_iff' : a / b < c / d ↔ a * d < c * b := by
  simpa only [div_eq_mul_inv] using mul_inv_lt_mul_inv_iff'

Division Inequality Equivalence: $\frac{a}{b} < \frac{c}{d} \leftrightarrow a d < c b$

Informal description

For elements $a, b, c, d$ in an ordered group, the inequality $\frac{a}{b} < \frac{c}{d}$ holds if and only if $a \cdot d < c \cdot b$.

lt_div_iff_mul_lt' theorem

: b < c / a ↔ a * b < c

Full source

@[to_additive]
theorem lt_div_iff_mul_lt' : b < c / a ↔ a * b < c := by rw [lt_div_iff_mul_lt, mul_comm]

Inequality equivalence: $b < c/a \leftrightarrow a \cdot b < c$

Informal description

For elements $a$, $b$, and $c$ in an ordered group, the inequality $b < c / a$ holds if and only if $a \cdot b < c$.

div_lt_iff_lt_mul' theorem

: a / b < c ↔ a < b * c

Full source

@[to_additive]
theorem div_lt_iff_lt_mul' : a / b < c ↔ a < b * c := by rw [div_lt_iff_lt_mul, mul_comm]

Division-Multiplication Inequality (Primed Version): $a / b < c \leftrightarrow a < b \cdot c$

Informal description

For elements $a$, $b$, and $c$ in an ordered group, the inequality $a / b < c$ holds if and only if $a < b \cdot c$.

inv_lt_div_iff_lt_mul' theorem

: b⁻¹ < a / c ↔ c < a * b

Full source

@[to_additive]
theorem inv_lt_div_iff_lt_mul' : b⁻¹b⁻¹ < a / c ↔ c < a * b :=
  lt_div_iff_mul_lt.trans inv_mul_lt_iff_lt_mul'

Inequality equivalence: $b^{-1} < a/c \leftrightarrow c < a \cdot b$

Informal description

For elements $a$, $b$, and $c$ in an ordered group, the inequality $b^{-1} < a / c$ holds if and only if $c < a \cdot b$.

div_lt_comm theorem

: a / b < c ↔ a / c < b

Full source

@[to_additive]
theorem div_lt_comm : a / b < c ↔ a / c < b :=
  div_lt_iff_lt_mul'.trans div_lt_iff_lt_mul.symm

Division Inequality Commutation: $a / b < c \leftrightarrow a / c < b$

Informal description

For elements $a$, $b$, and $c$ in an ordered group, the inequality $a / b < c$ holds if and only if $a / c < b$.

lt_div_comm theorem

: a < b / c ↔ c < b / a

Full source

@[to_additive]
theorem lt_div_comm : a < b / c ↔ c < b / a :=
  lt_div_iff_mul_lt'.trans lt_div_iff_mul_lt.symm

Inequality equivalence: $a < b/c \leftrightarrow c < b/a$

Informal description

For elements $a$, $b$, and $c$ in an ordered group, the inequality $a < b / c$ holds if and only if $c < b / a$.

div_lt_div'' theorem

(hab : a < b) (hcd : c < d) : a / d < b / c

Full source

@[to_additive (attr := gcongr) sub_lt_sub]
theorem div_lt_div'' (hab : a < b) (hcd : c < d) : a / d < b / c := by
  rw [div_eq_mul_inv, div_eq_mul_inv, mul_comm b, mul_inv_lt_inv_mul_iff, mul_comm]
  exact mul_lt_mul_of_lt_of_lt hab hcd

Inequality of Quotients under Componentwise Inequalities: $a < b$ and $c < d$ implies $a/d < b/c$

Informal description

For elements $a, b, c, d$ in an ordered group, if $a < b$ and $c < d$, then $a / d < b / c$.

lt_or_lt_of_div_lt_div theorem

: a / d < b / c → a < b ∨ c < d

Full source

@[to_additive] lemma lt_or_lt_of_div_lt_div : a / d < b / c → a < b ∨ c < d := by
  contrapose!; exact fun h ↦ div_le_div'' h.1 h.2

Disjunction from Quotient Inequality: $a/d < b/c$ implies $a < b$ or $c < d$

Informal description

For any elements $a, b, c, d$ in an ordered group, if $a / d < b / c$, then either $a < b$ or $c < d$.

cmp_div_one' theorem

[MulRightMono α] (a b : α) : cmp (a / b) 1 = cmp a b

Full source

@[to_additive (attr := simp) cmp_sub_zero]
theorem cmp_div_one' [MulRightMono α] (a b : α) :
    cmp (a / b) 1 = cmp a b := by rw [← cmp_mul_right' _ _ b, one_mul, div_mul_cancel]

Comparison of Quotient with One Equals Comparison of Elements in Right-Monotone Division Monoid

Informal description

Let $\alpha$ be a division monoid with a right-monotone multiplication. For any elements $a, b \in \alpha$, the comparison between $a / b$ and $1$ is equal to the comparison between $a$ and $b$, i.e., $\text{cmp}(a / b, 1) = \text{cmp}(a, b)$.

le_of_forall_one_lt_lt_mul theorem

(h : ∀ ε : α, 1 < ε → a < b * ε) : a ≤ b

Full source

@[to_additive]
theorem le_of_forall_one_lt_lt_mul (h : ∀ ε : α, 1 < ε → a < b * ε) : a ≤ b :=
  le_of_not_lt fun h₁ => lt_irrefl a (by simpa using h _ (lt_inv_mul_iff_lt.mpr h₁))

Order relation from multiplicative inequalities: $a \leq b$ via $a < b \cdot \varepsilon$ for all $\varepsilon > 1$

Informal description

For elements $a$ and $b$ in a division monoid, if for every $\varepsilon > 1$ we have $a < b \cdot \varepsilon$, then $a \leq b$.

le_iff_forall_one_lt_lt_mul theorem

: a ≤ b ↔ ∀ ε, 1 < ε → a < b * ε

Full source

@[to_additive]
theorem le_iff_forall_one_lt_lt_mul : a ≤ b ↔ ∀ ε, 1 < ε → a < b * ε :=
  ⟨fun h _ => lt_mul_of_le_of_one_lt h, le_of_forall_one_lt_lt_mul⟩

Characterization of Order via Multiplicative Inequalities: $a \leq b \leftrightarrow \forall \varepsilon > 1, a < b \cdot \varepsilon$

Informal description

For elements $a$ and $b$ in a division monoid, the inequality $a \leq b$ holds if and only if for every $\varepsilon > 1$, we have $a < b \cdot \varepsilon$.

div_le_inv_mul_iff theorem

[MulRightMono α] : a / b ≤ a⁻¹ * b ↔ a ≤ b

Full source

@[to_additive]
theorem div_le_inv_mul_iff [MulRightMono α] :
    a / b ≤ a⁻¹ * b ↔ a ≤ b := by
  rw [div_eq_mul_inv, mul_inv_le_inv_mul_iff]
  exact
    ⟨fun h => not_lt.mp fun k => not_lt.mpr h (mul_lt_mul_of_lt_of_lt k k), fun h =>
      mul_le_mul' h h⟩

Inequality Equivalence: $a / b \leq a^{-1} b \leftrightarrow a \leq b$

Informal description

For elements $a$ and $b$ in a division monoid $\alpha$ with right-monotone multiplication, the inequality $a / b \leq a^{-1} * b$ holds if and only if $a \leq b$.

div_le_div_flip theorem

{α : Type*} [CommGroup α] [LinearOrder α] [MulLeftMono α] {a b : α} : a / b ≤ b / a ↔ a ≤ b

Full source

@[to_additive]
theorem div_le_div_flip {α : Type*} [CommGroup α] [LinearOrder α]
    [MulLeftMono α] {a b : α} : a / b ≤ b / a ↔ a ≤ b := by
  rw [div_eq_mul_inv b, mul_comm]
  exact div_le_inv_mul_iff

Inequality Equivalence: $a / b \leq b / a \leftrightarrow a \leq b$

Informal description

For elements $a$ and $b$ in a commutative group $\alpha$ with a linear order and left-monotone multiplication, the inequality $a / b \leq b / a$ holds if and only if $a \leq b$.

Monotone.inv theorem

(hf : Monotone f) : Antitone fun x => (f x)⁻¹

Full source

@[to_additive]
theorem Monotone.inv (hf : Monotone f) : Antitone fun x => (f x)⁻¹ := fun _ _ hxy =>
  inv_le_inv_iff.2 (hf hxy)

Inverse of Monotone Function is Antitone

Informal description

If a function $f$ is monotone (i.e., order-preserving), then the function $x \mapsto (f(x))^{-1}$ is antitone (i.e., order-reversing).

Antitone.inv theorem

(hf : Antitone f) : Monotone fun x => (f x)⁻¹

Full source

@[to_additive]
theorem Antitone.inv (hf : Antitone f) : Monotone fun x => (f x)⁻¹ := fun _ _ hxy =>
  inv_le_inv_iff.2 (hf hxy)

Monotonicity of the Inverse of an Antitone Function

Informal description

If a function $f$ is antitone (i.e., order-reversing), then the function $x \mapsto (f(x))^{-1}$ is monotone (i.e., order-preserving).

MonotoneOn.inv theorem

(hf : MonotoneOn f s) : AntitoneOn (fun x => (f x)⁻¹) s

Full source

@[to_additive]
theorem MonotoneOn.inv (hf : MonotoneOn f s) : AntitoneOn (fun x => (f x)⁻¹) s :=
  fun _ hx _ hy hxy => inv_le_inv_iff.2 (hf hx hy hxy)

Inverse of Monotone Function is Antitone on Set

Informal description

For any function $f$ that is monotone on a set $s$, the function $x \mapsto (f(x))^{-1}$ is antitone on $s$.

AntitoneOn.inv theorem

(hf : AntitoneOn f s) : MonotoneOn (fun x => (f x)⁻¹) s

Full source

@[to_additive]
theorem AntitoneOn.inv (hf : AntitoneOn f s) : MonotoneOn (fun x => (f x)⁻¹) s :=
  fun _ hx _ hy hxy => inv_le_inv_iff.2 (hf hx hy hxy)

Monotonicity of the Inverse of an Antitone Function on a Set

Informal description

For any function $f$ that is antitone on a set $s$, the function $x \mapsto (f(x))^{-1}$ is monotone on $s$.

StrictMono.inv theorem

(hf : StrictMono f) : StrictAnti fun x => (f x)⁻¹

Full source

@[to_additive]
theorem StrictMono.inv (hf : StrictMono f) : StrictAnti fun x => (f x)⁻¹ := fun _ _ hxy =>
  inv_lt_inv_iff.2 (hf hxy)

Strict Monotonicity Implies Strict Antitonicity of Inverse

Informal description

If a function $f$ is strictly monotone, then the function $x \mapsto (f(x))^{-1}$ is strictly antitone.

StrictAnti.inv theorem

(hf : StrictAnti f) : StrictMono fun x => (f x)⁻¹

Full source

@[to_additive]
theorem StrictAnti.inv (hf : StrictAnti f) : StrictMono fun x => (f x)⁻¹ := fun _ _ hxy =>
  inv_lt_inv_iff.2 (hf hxy)

Inverse of Strictly Antitone Function is Strictly Monotone

Informal description

If a function $f$ is strictly antitone, then the function $x \mapsto (f(x))^{-1}$ is strictly monotone.

StrictMonoOn.inv theorem

(hf : StrictMonoOn f s) : StrictAntiOn (fun x => (f x)⁻¹) s

Full source

@[to_additive]
theorem StrictMonoOn.inv (hf : StrictMonoOn f s) : StrictAntiOn (fun x => (f x)⁻¹) s :=
  fun _ hx _ hy hxy => inv_lt_inv_iff.2 (hf hx hy hxy)

Inverse of Strictly Monotone Function is Strictly Antitone on Set

Informal description

If a function $f$ is strictly monotone on a set $s$, then the function $x \mapsto (f(x))^{-1}$ is strictly antitone on $s$.

StrictAntiOn.inv theorem

(hf : StrictAntiOn f s) : StrictMonoOn (fun x => (f x)⁻¹) s

Full source

@[to_additive]
theorem StrictAntiOn.inv (hf : StrictAntiOn f s) : StrictMonoOn (fun x => (f x)⁻¹) s :=
  fun _ hx _ hy hxy => inv_lt_inv_iff.2 (hf hx hy hxy)

Inverse of Strictly Antitone Function is Strictly Monotone

Informal description

If a function $f$ is strictly antitone on a set $s$, then the function $x \mapsto (f(x))^{-1}$ is strictly monotone on $s$.

Implementation details