norm_sq_eq

Mathlib.Analysis.CStarAlgebra.Module.Defs

URI: https://scilib.ai/kg/mathlib#CStarModule.norm_sq_eq

English

For all x in E, ‖x‖^2 = ‖⟪x,x⟫_A‖.

Русский

Для всех x в E верно: ||x||^2 = ||⟪x,x⟫_A||.

LaTeX

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

Lean4

theorem norm_sq_eq {x : E} : ‖x‖ ^ 2 = ‖⟪x, x⟫‖ := by simp [norm_eq_sqrt_norm_inner_self (A := A)]

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

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

Разделы

Аффилиация

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