inv_le_div_iff_le_mul' — Mathlib

English

Let α be a commutative group equipped with a left-compatible order. Then for all a, b, c in α, a^{-1} ≤ b/c if and only if c ≤ a b.

Русский

Пусть α — коммутативная группа, снабженная порядком, совместимым с умножением слева. Тогда для любых a, b, c ∈ α выполняется: a^{-1} ≤ b/c тогда и только если c ≤ a b.

LaTeX

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

Lean4

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

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