one_div_neg

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

English

In a linearly ordered group with zero, 1/a < 0 iff a < 0.

Русский

В линейно упорядоченной группе с нулём 1/a < 0 эквивалентно a < 0.

LaTeX

$$$1 / a < 0 \iff a < 0$$$

Lean4

theorem one_div_neg : 1 / a < 0 ↔ a < 0 :=
  one_div a ▸ inv_neg''

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

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

Разделы

Аффилиация

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