genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_le

English

If the generalized eigen-spaces stabilize after index k (i.e., maxUnifEigenspaceIndex ≤ k), then genEigenspace μ k = genEigenspace μ (maxUnifEigenspaceIndex μ).

Русский

Если индексы стабилизации достигнут при k, и maxUnifEigenspaceIndex μ ≤ k, то genEigenspace μ k = genEigenspace μ (maxUnifEigenspaceIndex μ).

LaTeX

$$f.genEigenspace μ k = f.genEigenspace μ (maxUnifEigenspaceIndex f μ) if maxUnifEigenspaceIndex f μ ≤ k$$

Lean4

/-- Generalized eigenspaces for exponents at least `finrank K V` are equal to each other. -/
theorem genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_le [IsNoetherian R M] (f : End R M) (μ : R) {k : ℕ}
    (hk : maxUnifEigenspaceIndex f μ ≤ k) : f.genEigenspace μ k = f.genEigenspace μ (maxUnifEigenspaceIndex f μ) :=
  le_antisymm (genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex _ _ _)
    ((f.genEigenspace μ).monotone <| by simpa using hk)

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