pi_norm_sq

Mathlib.Analysis.CStarAlgebra.Module.Constructions

URI: https://scilib.ai/kg/mathlib#WithCStarModule.pi_norm_sq

English

The square of the norm satisfies ‖x‖^2 = ‖∑_i ⟪x_i, x_i⟫_A‖.

Русский

Квадрат нормы удовлетворяет равенству ‖x‖^2 = ‖∑_i ⟪x_i, x_i⟫_A‖.

LaTeX

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

Lean4

theorem pi_norm_sq (x : C⋆ᵐᵒᵈ(A, Π i, E i)) : ‖x‖ ^ 2 = ‖∑ i, ⟪x i, x i⟫_A‖ := by simp [pi_norm]

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

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

Разделы

Аффилиация

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