mul_sub_mul_div_mul_neg_iff

Mathlib.Algebra.Order.Field.Basic

URI: https://scilib.ai/kg/mathlib#mul_sub_mul_div_mul_neg_iff

← MathLib Explorer

English

If c ≠ 0 and d ≠ 0, then (a d - b c)/(c d) < 0 iff a/c < b/d.

Русский

Пусть c ≠ 0 и d ≠ 0, тогда (a d - b c)/(c d) < 0 тогда и только тогда a/c < b/d.

LaTeX

$$(hc : c \neq 0) (hd : d \neq 0) : (a d - b c) / (c d) < 0 \iff a / c < b / d$$

Lean4

theorem mul_sub_mul_div_mul_neg_iff (hc : c ≠ 0) (hd : d ≠ 0) : (a * d - b * c) / (c * d) < 0 ↔ a / c < b / d := by
  rw [mul_comm b c, ← div_sub_div _ _ hc hd, sub_lt_zero]

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

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

Разделы

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

Аффилиация

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