English
For a nonunital ring A with a complex module structure, QuasispectrumRestricts a Complex.reCLM is equivalent to: every element x of the quasi-spectrum σ_n^C(a) satisfies x = x.re (i.e., x is real).
Русский
Для кольца A без единицы с модульной структурой над комплексами, QuasispectrumRestricts a Complex.reCLM эквивалентно тому, что каждый элемент x в кваспектре σ_n^C(a) удовлетворяет x = x.re (x реально).
LaTeX
$$$\text{QuasispectrumRestricts } a \ Complex.reCLM \iff \forall x \in \sigma_\nabla^{\mathbb{C}}(a), x = x_{\mathrm{re}}$$$
Lean4
theorem real_iff [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] {a : A} :
QuasispectrumRestricts a Complex.reCLM ↔ ∀ x ∈ σₙ ℂ a, x = x.re := by
rw [quasispectrumRestricts_iff_spectrumRestricts_inr, Unitization.quasispectrum_eq_spectrum_inr' _ ℂ,
SpectrumRestricts.real_iff]
