div_lt_div_iff'

Mathlib.Algebra.Order.Group.Unbundled.Basic

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

English

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

Русский

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

LaTeX

$$$\dfrac{a}{b} < \dfrac{c}{d} \iff ad < cb$$$

Lean4

@[to_additive sub_lt_sub_iff]
theorem div_lt_div_iff' : a / b < c / d ↔ a * d < c * b := by simpa only [div_eq_mul_inv] using mul_inv_lt_mul_inv_iff'

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

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

Разделы

Аффилиация

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