norm_mul_self_eq_normSq

Mathlib.Analysis.Complex.Norm

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

English

The square of the complex norm equals the squared magnitude: ‖z‖^2 = normSq z.

Русский

Квадрат модуля комплексного числа равен квадрату модуля: ‖z‖^2 = normSq z.

LaTeX

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

Lean4

theorem norm_mul_self_eq_normSq (z : ℂ) : ‖z‖ * ‖z‖ = normSq z :=
  Real.mul_self_sqrt (normSq_nonneg _)

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

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

Разделы

Аффилиация

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