im_inner_apply_self

Mathlib.Analysis.InnerProductSpace.Symmetric

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

English

If conj(c) = c, then c·T is symmetric whenever T is symmetric.

Русский

Если conj(c) = c, то c·T симметрично, когда T симметрично.

LaTeX

$$$ (c \cdot T).IsSymmetric $ if $ \overline{c} = c $ and $ T.IsSymmetric$$$

Lean4

@[simp]
theorem im_inner_apply_self {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (x : E) : im ⟪T x, x⟫ = 0 :=
  conj_eq_iff_im.mp <| hT.conj_inner_sym x x

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

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

Разделы

Аффилиация

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