real_inner_I_smul_self

Mathlib.Analysis.InnerProductSpace.Basic

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

English

For every x in E, the real inner product of x with i x is zero: ⟪x, i x⟫_ℝ = 0.

Русский

Для любого вектора x из E вещественное скалярное произведение ⟪x, i x⟫ равно нулю.

LaTeX

$$$\\langle x,i x\\rangle_{\\mathbb{R}} = 0.$$$

Lean4

theorem real_inner_I_smul_self (x : E) : (Inner.rclikeToReal 𝕜 E).inner x ((I : 𝕜) • x) = 0 := by
  simp [real_inner_eq_re_inner 𝕜, inner_smul_right]

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

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

Разделы

Аффилиация

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