inner_conj_symm

Mathlib.Analysis.InnerProductSpace.Defs

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

English

The inner product is conjugate symmetric: ⟪y,x⟫† = ⟪x,y⟫.

Русский

Скаля́рное произведение сопряжённо симметрично: ⟪y,x⟫† = ⟪x,y⟫.

LaTeX

$$$\\langle y,x\\rangle^{\\ast} = \\langle x,y\\rangle$$$

Lean4

theorem inner_conj_symm (x y : F) : ⟪y, x⟫† = ⟪x, y⟫ :=
  c.conj_inner_symm x y

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

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

Разделы

Аффилиация

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