chainTop_zero

Mathlib.Algebra.Lie.Weights.Chain

URI: https://scilib.ai/kg/mathlib#LieModule.chainTop_zero

English

For any natural n with n ≤ chainTopCoeff α β, the weight space genWeightSpace M (n•α + β) is not ⊥.

Русский

Для любого натурального n ≤ chainTopCoeff α β весовое пространство не равно ⊥.

LaTeX

$$$ n \\le \\text{chainTopCoeff}(α, β) \\Rightarrow genWeightSpace M (n \\cdot α + β) \\neq ⊥ $$$

Lean4

@[simp]
theorem chainTop_zero : chainTop 0 β = β := by ext; simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru