intCast_real_norm — Mathlib

English

For every Gaussian integer x ∈ ℤ[i], the real-valued norm of x coincides with the squared modulus of x when viewed as a complex number: (x.norm : ℝ) = Complex.normSq (x : ℂ).

Русский

Для любого гауссова целого x ∈ ℤ[i] нормa x, рассматриваемая как вещественное число, равна квадрату модуля x, считанного как комплекс: (x.norm : ℝ) = Complex.normSq (x : ℂ).

LaTeX

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

Lean4

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

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