maxGenEigenspace — Mathlib

English

The maximal generalized eigenspace for f and μ is the union of the kernels of (f − μ I)^k over all k ≥ 0.

Русский

Максимальное обобщённое эйгенпространство f для μ равно объединению ядер (f − μ I)^k по всем k ≥ 0.

LaTeX

$$$\\maxGenEigenspace(f, \\mu) = \\bigcup_{k \\in \\mathbb{N}} \\ker\\bigl((f - \\mu I)^k\\bigr).$$$

Lean4

/-- The union of the kernels of `(f - μ • id) ^ k` over all `k`. -/
abbrev maxGenEigenspace (f : End R M) (μ : R) : Submodule R M :=
  genEigenspace f μ ⊤

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