genWeightSpace_add_chainTop — Mathlib

English

If a root χ ≠ 0 lies in the root space of H, then the endomorphism toEnd K L M x is nilpotent for x in rootSpace H χ.

Русский

Если χ ≠ 0 принадлежит корневому пространству rootSpace H, тогда для x в rootSpace H χ соответствующий toEnd K L M x является нильпотентным.

LaTeX

$$$ χ ≠ 0 \\Rightarrow \\text{IsNilpotent}(\\text{toEnd}_K L M (x)) \\text{ for } x \\in \\text{rootSpace}(H, χ). $$$

Lean4

theorem genWeightSpace_add_chainTop : genWeightSpace M (α + chainTop α β : L → R) = ⊥ := by
  rw [coe_chainTop', ← add_assoc, ← succ_nsmul', genWeightSpace_chainTopCoeff_add_one_nsmul_add _ _ hα]

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