div_lt_iff_lt_mul'

Mathlib.Algebra.Order.Group.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#div_lt_iff_lt_mul'

English

For all a,b,c: a/b < c ↔ a < b c.

Русский

Для любых a,b,c: a/b < c ⇔ a < b c.

LaTeX

$$$\dfrac{a}{b} < c \iff a < b c$$$

Lean4

@[to_additive]
theorem div_lt_iff_lt_mul' : a / b < c ↔ a < b * c := by rw [div_lt_iff_lt_mul, mul_comm]

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

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

Разделы

Аффилиация

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