div_lt_iff_of_neg'

Mathlib.Algebra.Order.Field.Basic

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

English

If c < 0, then b/c < a iff c·a < b.

Русский

Если c < 0, то b/c < a эквивалентно c·a < b.

LaTeX

$$$c < 0 \rightarrow (\dfrac{b}{c} < a \iff c a < b)$$$

Lean4

theorem div_lt_iff_of_neg' (hc : c < 0) : b / c < a ↔ c * a < b := by rw [mul_comm, div_lt_iff_of_neg hc]

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

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

Разделы

Аффилиация

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