im_eq_zero_of_mem_spectrum — Mathlib

English

For a self-adjoint a, the imaginary part of every z ∈ spectrum(a) is zero.

Русский

Для сам-сопряженного a мнимая часть каждого z из спектра равна нулю.

LaTeX

$$$$\operatorname{im}(z) = 0 \quad \text{for all } z \in \operatorname{spectrum}_{\mathbb{C}}(a).$$$$

Lean4

/-- Any element of the spectrum of a selfadjoint is real. -/
theorem im_eq_zero_of_mem_spectrum {a : A} (ha : IsSelfAdjoint a) {z : ℂ} (hz : z ∈ spectrum ℂ a) : z.im = 0 := by
  rw [ha.mem_spectrum_eq_re hz, ofReal_im]

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