div_le_div_flip — Mathlib

English

Let α be a totally ordered commutative group in which left multiplication is order-preserving. Then for all a,b ∈ α, a/b ≤ b/a if and only if a ≤ b.

Русский

Пусть α — полностью упорядоченная коммутативная группа, в которой умножение слева сохраняет порядок. Тогда для любых a, b ∈ α выполняется a/b ≤ b/a тогда и только тогда, когда a ≤ b.

LaTeX

$$$ \forall a,b \in \alpha,\ \frac{a}{b} \le \frac{b}{a} \iff a \le b. $$$

Lean4

@[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

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