inner_im_symm

Mathlib.Analysis.InnerProductSpace.Defs

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

English

The imaginary part is antisymmetric: Im ⟪x,y⟫ = - Im ⟪y,x⟫.

Русский

Мнимая часть антисимметрична: Im ⟨x,y⟩ = - Im ⟨y,x⟩.

LaTeX

$$$\\\\Im\\\\langle x,y \\\\rangle = -\\\\Im\\\\langle y,x \\\\rangle$$$

Lean4

theorem inner_im_symm (x y : F) : im ⟪x, y⟫ = -im ⟪y, x⟫ := by rw [← inner_conj_symm, conj_im]

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

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

Разделы

Аффилиация

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