hasEigenvalueAt — Mathlib

English

For χ and x ∈ L, the endomorphism toEnd R L M x has eigenvalue χ(x).

Русский

Для χ и x ∈ L эндоморфизм toEnd x имеет собственное значение χ(x).

LaTeX

$$(toEnd R L M x).HasEigenvalue (χ x)$$

Lean4

theorem hasEigenvalueAt (χ : Weight R L M) (x : L) : (toEnd R L M x).HasEigenvalue (χ x) :=
  by
  obtain ⟨k : ℕ, hk : (toEnd R L M x).genEigenspace (χ x) k ≠ ⊥⟩ := by
    simpa [genWeightSpaceOf, ← Module.End.iSup_genEigenspace_eq] using χ.genWeightSpaceOf_ne_bot x
  exact Module.End.hasEigenvalue_of_hasGenEigenvalue hk

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