apply_clm — Mathlib

English

Let T be a symmetric linear map on a complex inner product space. Then for all x,y, ⟪T x, y⟫ = ⟪x, T y⟫.

Русский

Пусть T — симметричное линейное отображение векторного пространства со скалярным произведением. Тогда для всех x,y выполняется равенство ⟪T x, y⟫ = ⟪x, T y⟫.

LaTeX

$$$ \langle T x, y \rangle = \langle x, T y \rangle $$$

Lean4

@[simp]
theorem apply_clm {T : E →L[𝕜] E} (hT : IsSymmetric (T : E →ₗ[𝕜] E)) (x y : E) : ⟪T x, y⟫ = ⟪x, T y⟫ :=
  hT x y

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