instNorm — Mathlib

English

Let z be a complex number. The norm on the complex numbers is defined by ‖z‖ = √(normSq z). In particular, this magnitude agrees with the usual Euclidean length.

Русский

Пусть z — комплексное число. Норма на комплексных числах задаётся как ‖z‖ = √(normSq z). В частности, величина совпадает с обычной евклидовой длиной.

LaTeX

$$$\forall z \in \mathbb{C},\; \|z\| = \sqrt{\operatorname{normSq}(z)}$$$

Lean4

instance instNorm : Norm ℂ where norm z := √(normSq z)

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