genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex

English

For Noetherian R-modules, f.genEigenspace μ k ⊆ f.genEigenspace μ (maxUnifEigenspaceIndex μ).

Русский

Для [IsNoetherian] f.genEigenspace μ k ⊆ f.genEigenspace μ (maxUnifEigenspaceIndex μ).

LaTeX

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

Lean4

theorem genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex [IsNoetherian R M] (f : End R M) (μ : R) (k : ℕ∞) :
    f.genEigenspace μ k ≤ f.genEigenspace μ (maxUnifEigenspaceIndex f μ) :=
  by
  rw [← genEigenspace_top_eq_maxUnifEigenspaceIndex]
  exact (f.genEigenspace μ).monotone le_top

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