zero_genWeightSpace_eq_top_of_nilpotent'

English

In a Noetherian Lie module, for χ and x ∈ L there exists k such that genWeightSpace M χ is contained in the kernel of (toEnd x − algebraMap χ x)^k.

Русский

В конечно экземпляре Ли-модуля существует k such that genWeightSpace M χ ⊆ ker((toEnd x − algebraMap χ x)^k).

LaTeX

$$∃ k, genWeightSpace M χ ≤ ker ((toEnd R L M x − algebraMap R _ (χ x))^k)$$

Lean4

/-- See also the more useful form `LieModule.zero_genWeightSpace_eq_top_of_nilpotent`. -/
@[simp]
theorem zero_genWeightSpace_eq_top_of_nilpotent' [IsNilpotent L M] : genWeightSpace M (0 : L → R) = ⊤ := by
  simp [genWeightSpace, genWeightSpaceOf]

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