div_lt_iff₀'

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#div_lt_iff₀'

← MathLib Explorer

English

Let the right divisor c satisfy c > 0. Then b / c < a if and only if b < c · a.

Русский

Пусть 0 < c. Тогда b / c < a эквивалентно b < c · a.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru