inner_re_symm

Mathlib.Analysis.InnerProductSpace.Basic

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

English

The real part of ⟪x,y⟫ is symmetric: Re⟪x,y⟫ = Re⟪y,x⟫.

Русский

Действительная часть скалярного произведения симметрична: Re⟪x,y⟫ = Re⟪y,x⟫.

LaTeX

$$$\operatorname{Re}\langle x, y\rangle = \operatorname{Re}\langle y, x\rangle$$$

Lean4

theorem inner_re_symm (x y : E) : re ⟪x, y⟫ = re ⟪y, x⟫ := by rw [← inner_conj_symm, conj_re]

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

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

Разделы

Аффилиация

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