iSup_ucs_le_genWeightSpace_zero — Mathlib

English

The action of L via toEnd on the weight space has eigenvalues given by weight χ.

Русский

Действие L через toEnd на весовом пространстве имеет собственные значения, задаваемые χ.

LaTeX

$$hasEigenvalueAt χ x$$

Lean4

theorem iSup_ucs_le_genWeightSpace_zero : ⨆ k, (⊥ : LieSubmodule R L M).ucs k ≤ genWeightSpace M (0 : L → R) := by
  simpa using LieSubmodule.ucs_le_of_normalizer_eq_self (genWeightSpace_zero_normalizer_eq_self R L M)

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