hasUnifEigenvalue_iff_mem_spectrum

English

For any f, μ with HasUnifEigenvalue μ 1, μ belongs to spectrum K f.

Русский

Для любого f и μ с HasUnifEigenvalue μ 1, μ принадлежит спектру f.

LaTeX

$$HasUnifEigenvalue(f, μ, 1) → μ ∈ spectrum(f)$$

Lean4

theorem hasUnifEigenvalue_iff_mem_spectrum [FiniteDimensional K V] {f : End K V} {μ : K} :
    f.HasUnifEigenvalue μ 1 ↔ μ ∈ spectrum K f :=
  by
  rw [spectrum.mem_iff, IsUnit.sub_iff, LinearMap.isUnit_iff_ker_eq_bot, HasUnifEigenvalue, genEigenspace_one, ne_eq,
    not_iff_not]
  simp [Submodule.ext_iff, LinearMap.mem_ker]

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