norm_pos

Mathlib.NumberTheory.Zsqrtd.GaussianInt

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

English

The norm is positive exactly when the Gaussian integer is nonzero.

Русский

Норма положительна тогда и только тогда, когда гауссова целая ненулевая.

LaTeX

$$$ 0 < \operatorname{norm}(x) \iff x \neq 0 $$$

Lean4

theorem norm_pos {x : ℤ[i]} : 0 < norm x ↔ x ≠ 0 := by rw [lt_iff_le_and_ne, Ne, eq_comm, norm_eq_zero];
  simp [norm_nonneg]

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

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

Разделы

Аффилиация

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