normSq — Mathlib

English

The norm-squared of a complex number equals the sum of squares of its real and imaginary parts.

Русский

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

LaTeX

$$$\operatorname{normSq}(z) = z_{\mathrm{re}}^2 + z_{\mathrm{im}}^2$$$

Lean4

/-- The norm squared function. -/
@[pp_nodot]
def normSq : ℂ →*₀ ℝ where
  toFun z := z.re * z.re + z.im * z.im
  map_zero' := by simp
  map_one' := by simp
  map_mul' z
    w := by
    dsimp
    ring

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