English
An element m belongs to genWeightSpace M χ if and only if for every x ∈ L there exists k such that ((toEnd x - χ(x) Id)^k) m = 0; equivalently m lies in all generalized χ(x)-eigenspaces for the operators toEnd x.
Русский
Элемент m принадлежит genWeightSpace M χ тогда и только тогда, когда для каждого x ∈ L существует k такое, что ((toEnd x − χ(x)) Id)^k m = 0; иначе говоря, m лежит во всех общих обобщенных χ(x)-собственных пространствах операторов toEnd x.
LaTeX
$$$ m \\in \\mathrm{genWeightSpace}(M, χ) \\iff \\forall x \\exists k: ((\\mathrm{toEnd}\\;R\\;L\\;M\\;x - χ(x) \\mathrm{Id})^k) m = 0 $$$
Lean4
theorem mem_genWeightSpace (χ : L → R) (m : M) :
m ∈ genWeightSpace M χ ↔ ∀ x, ∃ k : ℕ, ((toEnd R L M x - χ x • ↑1) ^ k) m = 0 := by
simp [genWeightSpace, mem_genWeightSpaceOf]
