inv_neg''

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

English

For a group with zero and a linear order, a^{-1} < 0 iff a < 0.

Русский

Для упорядоченной группы с нулём верно: a^{-1} < 0 ⇔ a < 0.

LaTeX

$$$a^{-1} < 0 \iff a < 0$$$

Lean4

@[simp]
theorem inv_neg'' : a⁻¹ < 0 ↔ a < 0 := by have := PosMulMono.toPosMulReflectLT (α := G₀);
  simp only [← not_le, inv_nonneg]

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

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

Разделы

Аффилиация

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