isSelfAdjoint — Mathlib

English

If E is finite-dimensional over 𝕜 and T is positive, then T is self-adjoint.

Русский

Если пространство E конечномерно над 𝕜 и T положителен, то T является самосопряжённым.

LaTeX

$$$[\\text{FiniteDimensional}]\\ (T\\text{ positive})\\Rightarrow \\text{IsSelfAdjoint}(T).$$$

Lean4

theorem isSelfAdjoint [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : IsPositive T) : IsSelfAdjoint T :=
  (isSymmetric_iff_isSelfAdjoint _).mp hT.isSymmetric

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