English
For semifield 𝕜 and algebra A with NonnegSpectrumClass 𝕜 A, the nonnegativity of a is equivalent to all spectrum values being nonnegative.
Русский
Для полей 𝕜 и алгебры A эквивалентно: если a ≥ 0, то все значения спектра спектра 𝕜 a не отрицательны.
LaTeX
$$NonnegSpectrumClass 𝕜 A ↔ ∀ a, 0 ≤ a → ∀ x ∈ spectrum 𝕜 a, 0 ≤ x$$
Lean4
theorem iff_spectrum_nonneg {𝕜 A : Type*} [Semifield 𝕜] [LinearOrder 𝕜] [Ring A] [PartialOrder A] [Algebra 𝕜 A] :
NonnegSpectrumClass 𝕜 A ↔ ∀ a : A, 0 ≤ a → ∀ x ∈ spectrum 𝕜 a, 0 ≤ x := by
simp [show NonnegSpectrumClass 𝕜 A ↔ _ from ⟨fun ⟨h⟩ ↦ h, (⟨·⟩)⟩, quasispectrum_eq_spectrum_union_zero]