abs_natCast_norm

Mathlib.NumberTheory.Zsqrtd.GaussianInt

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

English

The integer natAbs of the real-valued norm equals the norm, i.e., the norm is nonnegative.

Русский

Модуль целого числа нормa равен самой норме: норма неотрицательна.

LaTeX

$$$ (x.norm.natAbs : \mathbb{Z}) = x.norm $$$

Lean4

theorem abs_natCast_norm (x : ℤ[i]) : (x.norm.natAbs : ℤ) = x.norm :=
  Int.natAbs_of_nonneg (norm_nonneg _)

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

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

Разделы

Аффилиация

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