div_le_iff_le_mul — Mathlib

English

In a commutative group with order, a*b^{-1} ≤ c*d^{-1} is equivalent to a*d ≤ c*b.

Русский

В коммутативной группе с порядком: a*b^{-1} ≤ c*d^{-1} эквивалентно a*d ≤ c*b.

LaTeX

$$$a b^{-1} \le c d^{-1} \iff a d \le c b$$$

Lean4

@[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]
    -- Note: we intentionally don't have `@[simp]` for the additive version,
    -- since the LHS simplifies with `tsub_le_iff_right`

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