le_div_iff_of_neg'

Mathlib.Algebra.Order.Field.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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