UnifEigenvalues — Mathlib

English

For a fixed endomorphism f and index k, UnifEigenvalues(f,k) is the set of μ ∈ R such that f has μ as a uniform eigenvalue at k.

Русский

Для данного концевого отображения f и индекса k множество UnifEigenvalues(f,k) состоит из всех μ ∈ R, таких что μ является унифицированным собственным значением f при k.

LaTeX

$$UnifEigenvalues(f,k) := { μ ∈ R // f.HasUnifEigenvalue μ k }$$

Lean4

/-- Let `M` be an `R`-module, and `f` an `R`-linear endomorphism of `M`.
For `k : ℕ∞`, we define `UnifEigenvalues f k` to be the type of all
`μ : R` that satisfy `f.HasUnifEigenvalue μ k`.

For `k = 1` this is the type of all eigenvalues of `f`. -/
def UnifEigenvalues (f : End R M) (k : ℕ∞) : Type _ :=
  { μ : R // f.HasUnifEigenvalue μ k }

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