natAbs_norm_eq — Mathlib

English

The natAbs of the norm equals the sum of squares of the absolute values of the real and imaginary parts: norm(x).natAbs = (re x).natAbs^2 + (im x).natAbs^2.

Русский

Пусть x = a + bi; тогда |norm(x)| = |a|^2 + |b|^2, т.е. natAbs нормы равна сумме квадратов абсолютных частей.

LaTeX

$$$ x.norm.natAbs = x.re.natAbs^2 + x.im.natAbs^2 $$$

Lean4

theorem natAbs_norm_eq (x : ℤ[i]) : x.norm.natAbs = x.re.natAbs * x.re.natAbs + x.im.natAbs * x.im.natAbs :=
  by
  zify
  rw [abs_norm (by simp)]
  simp [Zsqrtd.norm]

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