isSelfAdjoint — Mathlib

English

If the quasispectrum of a is restricted, then a is self-adjoint.

Русский

Если квази-спектр ограничен, то элемент самосопряжен.

LaTeX

$$$$ \\text{QuasispectrumRestricts}(a, \\dots) \\Rightarrow \\text{IsSelfAdjoint}(a) $$$$

Lean4

/-- A normal element whose `ℂ`-quasispectrum is contained in `ℝ` is selfadjoint. -/
theorem isSelfAdjoint (a : A) (ha : QuasispectrumRestricts a Complex.reCLM) [IsStarNormal a] : IsSelfAdjoint a :=
  isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts.mpr ⟨‹_›, ha⟩

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