mul_lt_mul_left_of_neg

Mathlib.Algebra.Order.Ring.Unbundled.Basic

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

← MathLib Explorer

English

If c < 0, then c*a < c*b iff b < a.

Русский

Если c < 0, то c*a < c*b тогда и только тогда, когда b < a.

LaTeX

$$$c < 0 \Rightarrow (c a < c b \iff b < a)$$$

Lean4

@[simp]
theorem mul_lt_mul_left_of_neg [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R]
    {a b c : R} (h : c < 0) : c * a < c * b ↔ b < a :=
  (strictAnti_mul_left h).lt_iff_gt

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

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

Разделы

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

Аффилиация

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