normUnit_eq

Mathlib.Algebra.GCDMonoid.Nat

URI: https://scilib.ai/kg/mathlib#Int.normUnit_eq

English

The norm unit is the sign indicator: normUnit(z) = 1 for z ≥ 0 and -1 for z < 0.

Русский

Единица нормализации — знаковая функция: normUnit(z) = 1 при z ≥ 0 и −1 при z < 0.

LaTeX

$$$\operatorname{normUnit}(z) = \begin{cases}1, & z \ge 0 \\ -1, & z < 0\end{cases}$$$

Lean4

theorem normUnit_eq (z : ℤ) : normUnit z = if 0 ≤ z then 1 else -1 :=
  rfl

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

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

Разделы

Аффилиация

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