intCast_complex_norm

Mathlib.NumberTheory.Zsqrtd.GaussianInt

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

English

For every x ∈ ℤ[i], the complex value of x.norm equals Complex.normSq (x : ℂ).

Русский

Для каждого x ∈ ℤ[i] комплексное значение x.norm равно Complex.normSq (x : ℂ).

LaTeX

$$$ (x.norm : \mathbb{C}) = \operatorname{normSq}(x : \mathbb{C}) $$$

Lean4

@[simp]
theorem intCast_complex_norm (x : ℤ[i]) : (x.norm : ℂ) = Complex.normSq (x : ℂ) := by cases x; rw [Zsqrtd.norm, normSq];
  simp

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

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

Разделы

Аффилиация

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