normSq_eq_def'

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.normSq_eq_def'

English

The squared norm is equal to the squared usual norm: normSq(z) = ‖z‖^2.

Русский

Квадрат нормы равен квадрату обычной нормы: normSq(z) = ‖z‖^2.

LaTeX

$$$$\\operatorname{normSq}(z) = \\|z\\|^{2}.$$$$

Lean4

theorem normSq_eq_def' (z : K) : normSq z = ‖z‖ ^ 2 :=
  norm_sq_eq_def.symm

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

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

Разделы

Аффилиация

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