norm_def

Mathlib.Analysis.Complex.Norm

URI: https://scilib.ai/kg/mathlib#Complex.norm_def

English

For every complex z, the complex norm equals the square root of the squared magnitude: ‖z‖ = √(normSq z).

Русский

Для каждого z ∈ ℂ модуль равен корню квадратному из квадрата модуля: ‖z‖ = √(normSq z).

LaTeX

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

Lean4

theorem norm_def (z : ℂ) : ‖z‖ = √(normSq z) :=
  rfl

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

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

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru