im_inner_self_apply

Mathlib.Analysis.InnerProductSpace.Symmetric

URI: https://scilib.ai/kg/mathlib#LinearMap.IsSymmetric.im_inner_self_apply

English

For symmetric T, the imaginary part of ⟪T x, x⟫ is zero for all x.

Русский

Для симметричного T мнимая часть ⟪T x, x⟫ равна нулю для всех x.

LaTeX

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

Lean4

@[simp]
theorem im_inner_self_apply {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (x : E) : im ⟪x, T x⟫ = 0 := by simp [← hT x x, hT]

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

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

Разделы

Аффилиация

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