isSymmetric_iff_sesqForm — Mathlib

English

A (not necessarily bounded) operator T on an inner product space is symmetric if and only if ⟪Tx,y⟫ = ⟪x,Ty⟫ for all x,y.

Русский

Оператор T над пространством с скалярным произведением симметричен тогда и только тогда, когда для всех x,y выполнено ⟪Tx,y⟫ = ⟪x,Ty⟫.

LaTeX

$$$\forall x,y\;\langle Tx, y\rangle = \langle x, Ty\rangle$$$

Lean4

/-- An operator `T` on an inner product space is symmetric if and only if it is
`LinearMap.IsSelfAdjoint` with respect to the sesquilinear form given by the inner product. -/
theorem isSymmetric_iff_sesqForm (T : E →ₗ[𝕜] E) :
    T.IsSymmetric ↔ LinearMap.IsSelfAdjoint (R := 𝕜) (M := E) sesqFormOfInner T :=
  ⟨fun h x y => (h y x).symm, fun h x y => (h y x).symm⟩

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