norm_nonneg

Mathlib.NumberTheory.Zsqrtd.GaussianInt

URI: https://scilib.ai/kg/mathlib#GaussianInt.norm_nonneg

English

For every Gaussian integer x, the norm is nonnegative: 0 ≤ norm x.

Русский

Для каждого гауссова целого x норма неотрицательна: 0 ≤ norm x.

LaTeX

$$$ 0 \le \operatorname{norm}(x) $$$

Lean4

theorem norm_nonneg (x : ℤ[i]) : 0 ≤ norm x :=
  Zsqrtd.norm_nonneg (by simp) _

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

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

Разделы

Аффилиация

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