chainBot_neg

Mathlib.Algebra.Lie.Weights.Chain

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

English

The weight space of −α + chainBot(α, β) is trivial, i.e., genWeightSpace M (−α + chainBot(α, β)) = ⊥.

Русский

Весовое пространство −α + chainBot(α, β) тривиально.

LaTeX

$$$ genWeightSpace M ( -α + \\text{chainBot}(α, β) ) = ⊥ $$$

Lean4

@[simp]
theorem chainBot_neg : chainBot (-α) β = chainTop α β := by ext; simp

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

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

Разделы

Аффилиация

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