inner_re_symm

Mathlib.Analysis.InnerProductSpace.Defs

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

English

The real part satisfies Re ⟪x,y⟫ = Re ⟪y,x⟫.

Русский

Действительная часть удовлетворяет Re ⟨x,y⟩ = Re ⟨y,x⟩.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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