inner_smul_real_right

Mathlib.Analysis.InnerProductSpace.Basic

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

English

The imaginary part changes sign on swap: Im⟪x,y⟫ = −Im⟪y,x⟫.

Русский

Мнимая часть меняет знак при перестановке: Im⟪x,y⟫ = −Im⟪y,x⟫.

LaTeX

$$$\operatorname{Im}\langle x, y\rangle = -\operatorname{Im}\langle y, x\rangle$$$

Lean4

theorem inner_smul_real_right (x y : E) (r : ℝ) : ⟪x, (r : 𝕜) • y⟫ = r • ⟪x, y⟫ := by
  rw [inner_smul_right, Algebra.smul_def]

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

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

Разделы

Аффилиация

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