adjoint_eq — Mathlib

English

Let E be a finite-dimensional inner product space over a complex field and T: E → E be a positive linear map. Then T is self-adjoint, i.e., T* = T.

Русский

Пусть E — конечномерное пространство с скалярным произведением, над комплексным полем, и T: E → E — положительное линейное отображение. Тогда T самосопряжено: T* = T.

LaTeX

$$$$\text{Let } E \text{ be finite-dimensional over } \mathbb{K}, \ T \in \mathrm{End}_{\mathbb{K}}(E), \text{ and } T \text{ is positive }\\\Rightarrow T^{*} = T.$$$$

Lean4

theorem adjoint_eq [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : IsPositive T) : T.adjoint = T :=
  hT.isSelfAdjoint

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