zero_lt

Mathlib.Algebra.Order.GroupWithZero.Canonical

URI: https://scilib.ai/kg/mathlib#Units.zero_lt

English

Every unit in a linear ordered group with zero is strictly positive; that is, 0 < u for any unit u.

Русский

Каждая единица в линейно упорядоченной группе с нулём положительна; то есть 0 < u для любой единицы u.

LaTeX

$$$\\\\forall u \\\\in \\\\alpha^{\\\\times}, \\\\ 0 < u$$$

Lean4

@[simp]
theorem zero_lt (u : αˣ) : (0 : α) < u :=
  zero_lt_iff.2 u.ne_zero

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

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

Разделы

Аффилиация

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