inner_self_im

Mathlib.Analysis.InnerProductSpace.Basic

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

English

For every vector x in E, the imaginary part of ⟪x, x⟫ is zero.

Русский

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

LaTeX

$$$\operatorname{Im}\langle x, x\rangle = 0$$$

Lean4

@[simp]
theorem inner_self_im (x : E) : im ⟪x, x⟫ = 0 := by rw [← @ofReal_inj 𝕜, im_eq_conj_sub]; simp

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

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

Разделы

Аффилиация

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