norm_inner_symm

Mathlib.Analysis.InnerProductSpace.Defs

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

English

Re(⟪x,y⟫ ⟪y,x⟫) = ||⟪x,y⟫ ⟪y,x⟫||.

Русский

Re(⟨x,y⟩ ⟨y,x⟫) = |⟨x,y⟩⟨y,x⟩|.

LaTeX

$$$\\\\Re\\\\left(\\\\langle x,y \\\\rangle \\\\langle y,x \\\\rangle\\right) = \\\\|\\\\langle x,y \\\\rangle \\\\langle y,x \\\\rangle\\\\|$$$

Lean4

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

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

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

Разделы

Аффилиация

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