normSq — Mathlib

English

The norm-squared map n(z) is the real-valued function sending z to Re(z)^2 + Im(z)^2; i.e., z ↦ (Re z)^2 + (Im z)^2.

Русский

Отображение на норму в квадрате определяется как z ↦ (Re z)^2 + (Im z)^2.

LaTeX

$$$$\\|z\\|^{2} = (\\operatorname{Re}(z))^{2} + (\\operatorname{Im}(z))^{2}.$$$$

Lean4

/-- The norm squared function. -/
def normSq : K →*₀ ℝ where
  toFun z := re z * re z + im z * im z
  map_zero' := by simp only [add_zero, mul_zero, map_zero]
  map_one' := by simp only [one_im, add_zero, mul_one, one_re, mul_zero]
  map_mul' z
    w := by
    simp only [mul_im, mul_re]
    ring

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