coe_re_inner_self_apply

Mathlib.Analysis.InnerProductSpace.Symmetric

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

English

For symmetric T, the real part of ⟪x, T x⟫ equals ⟪x, T x⟫ for all x.

Русский

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

LaTeX

$$$ \operatorname{Re}\langle x, T x \rangle = \langle x, T x \rangle $$$

Lean4

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

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

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

Разделы

Аффилиация

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