sq_norm

Mathlib.Analysis.Complex.Norm

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

English

The square of the norm equals normSq, i.e., ||z||^2 = normSq(z).

Русский

Квадрат нормы равен normSq: ||z||^2 = normSq(z).

LaTeX

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

Lean4

protected theorem sq_norm (z : ℂ) : ‖z‖ ^ 2 = normSq z :=
  (normSq_eq_norm_sq z).symm

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

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

Разделы

Аффилиация

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