HasUnifEigenvalue — Mathlib

English

A scalar μ is a uniform eigenvalue of f at index k if the μ-generalized eigenspace is nontrivial, i.e., it is not the bottom submodule.

Русский

Число μ является унифицированным собственным значением f при индексе k тогда и только тогда, когда μ-обобщённое собственное пространство непусто, то есть не равно нижнему подполнению.

LaTeX

$$HasUnifEigenvalue(f, μ, k) := f.genEigenspace(μ, k) ≠ ⊥$$

Lean4

/-- Let `M` be an `R`-module, and `f` an `R`-linear endomorphism of `M`.
Then `μ : R` and `k : ℕ∞` satisfy `HasUnifEigenvalue f μ k` if
`f.genEigenspace μ k ≠ ⊥`.

For `k = 1`, this means that `μ` is an eigenvalue of `f`. -/
def HasUnifEigenvalue (f : End R M) (μ : R) (k : ℕ∞) : Prop :=
  f.genEigenspace μ k ≠ ⊥

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