English
Let A be a complex algebra; then SpectrumRestricts a Complex.reCLM holds if and only if every spectral value x in spectrum ℂ a satisfies x = x.re (i.e., x is real).
Русский
Пусть A — комплексная алгебра. Утверждение SpectrumRestricts a Complex.reCLM истинно тогда и только тогда, когда для каждого значения спектра x ∈ spectrum ℂ a выполняется x = Re(x) (x реально).
LaTeX
$$$\text{SpectrumRestricts } a \ Complex.reCLM \iff \forall x \in \sigma_{\mathbb{C}}(a), x = x_{\mathrm{re}}$$$
Lean4
theorem real_iff [Algebra ℂ A] {a : A} : SpectrumRestricts a Complex.reCLM ↔ ∀ x ∈ spectrum ℂ a, x = x.re :=
by
refine ⟨fun h x hx ↦ ?_, fun h ↦ ?_⟩
· obtain ⟨x, -, rfl⟩ := h.algebraMap_image.symm ▸ hx
simp
· exact .of_subset_range_algebraMap Complex.ofReal_re fun x hx ↦ ⟨x.re, (h x hx).symm⟩
