Some lemmas on the spectrum and quasispectrum of elements and positivity on ℂ

theorem SpectrumRestricts.real_iff {A : Type u_1} [Ring A] [Algebra ℂ A] {a : A} : SpectrumRestricts a ⇑Complex.reCLM ↔ ∀ x ∈ spectrum ℂ a, x = ↑x.re

theorem QuasispectrumRestricts.real_iff {A : Type u_1} [NonUnitalRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] {a : A} : QuasispectrumRestricts a ⇑Complex.reCLM ↔ ∀ x ∈ quasispectrum ℂ a, x = ↑x.re