ofReal_normSq_eq_inner_self

Mathlib.Analysis.InnerProductSpace.Defs

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

← MathLib Explorer

English

For every x, the squared norm equals the inner product with itself: ∥x∥^2 = ⟪x, x⟫.

Русский

Для каждого x: ∥x∥^2 = ⟪x, x⟫.

LaTeX

$$$\\\\|x\\\\|^2 = \\\\langle x, x \\\\rangle$$$

Lean4

theorem ofReal_normSq_eq_inner_self (x : F) : (normSqF x : 𝕜) = ⟪x, x⟫ :=
  by
  rw [ext_iff]
  exact ⟨by simp only [ofReal_re, normSq], by simp only [inner_self_im, ofReal_im]⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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