normSq

Mathlib.Analysis.InnerProductSpace.Defs

URI: https://scilib.ai/kg/mathlib#InnerProductSpace.Core.normSq

English

The squared norm on F is given by the real part of ⟪x,x⟫, i.e., normSq(x) = Re⟪x,x⟫.

Русский

Квадрат нормы на F задаётся как вещественная часть скалярного произведения: normSq(x) = Re⟪x,x⟫.

LaTeX

$$$\\text{normSq}(x) := \\Re \\langle x,x \\rangle$$$

Lean4

/-- The norm squared function for `PreInnerProductSpace.Core` structure. -/
def normSq (x : F) :=
  re ⟪x, x⟫

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

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

Разделы

Аффилиация

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