mem_spectrum — Mathlib

English

There is a canonical coercion from UnifEigenvalues(f,k) to R given by val.

Русский

Существует каноническое преобразование из множества UnifEigenvalues(f,k) в R, задаваемое функцией val.

LaTeX

$$instCoeOut {f} {k} : CoeOut (UnifEigenvalues f k) R$$

Lean4

theorem mem_spectrum {f : End R M} {μ : R} (hμ : HasUnifEigenvalue f μ 1) : μ ∈ spectrum R f :=
  by
  refine spectrum.mem_iff.mpr fun h_unit ↦ ?_
  set f' := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
  rcases hμ.exists_hasUnifEigenvector with ⟨v, hv⟩
  refine hv.2 ((LinearMap.ker_eq_bot'.mp f'.ker) v (?_ : μ • v - f v = 0))
  rw [hv.apply_eq_smul, sub_self]

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