conj_inner_sym — Mathlib

English

Let T be a symmetric linear map on a complex inner product space. Then for all x and y, the conjugate of the inner product ⟪T x, y⟫ equals ⟪T y, x⟫.

Русский

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

LaTeX

$$$ \overline{\langle T x, y \rangle} = \langle T y, x \rangle $$$

Lean4

theorem conj_inner_sym {T : E →ₗ[𝕜] E} (hT : IsSymmetric T) (x y : E) : conj ⟪T x, y⟫ = ⟪T y, x⟫ := by
  rw [hT x y, inner_conj_symm]

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