smul_neg_iff_of_neg_left

Mathlib.Algebra.Order.Module.Defs

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

← MathLib Explorer

English

0 ≤ a·b iff 0 ≤ a and 0 ≤ b or a ≤ 0 and b ≤ 0.

Русский

0 ≤ a·b тогда и только тогда, когда либо 0 ≤ a и 0 ≤ b, либо a ≤ 0 и b ≤ 0.

LaTeX

$$$0 \le a \cdot b \iff (0 \le a \land 0 \le b) \lor (a \le 0 \land b \le 0)$$$

Lean4

theorem smul_neg_iff_of_neg_left (ha : a < 0) : a • b < 0 ↔ 0 < b := by
  simpa only [smul_zero] using smul_lt_smul_iff_of_neg_left ha (b₂ := (0 : β))

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

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

Разделы

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

Аффилиация

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