lt_div_iff₀' — Mathlib

English

Let the group be ordered and c > 0. Then a < b / c if and only if c · a < b.

Русский

Пусть имеется упорядоченная комм-группа с нулём и c > 0. Тогда a < b / c эквивалентно c · a < b.

LaTeX

$$$0 < c \rightarrow\ (a < b/c \iff c \cdot a < b)$$$

Lean4

/-- See `lt_div_iff₀` for a version with multiplication on the other side. -/
theorem lt_div_iff₀' (hc : 0 < c) : a < b / c ↔ c * a < b := by rw [lt_div_iff₀ hc, mul_comm]

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