div_le_inv_mul_iff — Mathlib

English

In a group with appropriate monotonicity, a/b ≤ a^{-1} b ⇔ a ≤ b.

Русский

В группе с подходящей монотонностью выполняется a/b ≤ a^{-1} b ⇔ a ≤ b.

LaTeX

$$$a/b \le a^{-1} b \iff a \le b$$$

Lean4

@[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⟩
      -- What is the point of this lemma?  See comment about `div_le_inv_mul_iff` above.
      -- Note: we intentionally don't have `@[simp]` for the additive version,
      -- since the LHS simplifies with `tsub_le_iff_right`

Похожие утверждения