normSq_eq_norm_sq

Mathlib.Analysis.Complex.Norm

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

English

For any complex z, the squared norm equals the square of the modulus: normSq(z) = ||z||^2.

Русский

Для любого комплексного числа z квадрат нормы равен квадрату модуля: normSq(z) = |z|^2.

LaTeX

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

Lean4

theorem normSq_eq_norm_sq (z : ℂ) : normSq z = ‖z‖ ^ 2 := by simp [norm_def, sq, Real.mul_self_sqrt (normSq_nonneg _)]

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

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

Разделы

Аффилиация

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