norm_inner_symm

Mathlib.Analysis.InnerProductSpace.Basic

URI: https://scilib.ai/kg/mathlib#norm_inner_symm

English

The norm of ⟪x,y⟫ equals the norm of ⟪y,x⟫: ‖⟪x,y⟫‖ = ‖⟪y,x⟫‖.

Русский

Норма скалярного произведения ⟪x,y⟫ равна норме ⟪y,x⟫: ‖⟪x,y⟫‖ = ‖⟪y,x⟫‖.

LaTeX

$$$\|\langle x, y \rangle\| = \|\langle y, x \rangle\|$$$

Lean4

theorem norm_inner_symm (x y : E) : ‖⟪x, y⟫‖ = ‖⟪y, x⟫‖ := by rw [← inner_conj_symm, norm_conj]

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

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

Разделы

Аффилиация

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