chainTop_neg

Mathlib.Algebra.Lie.Weights.Chain

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

English

Negating α swaps top and bottom roles: chainTop(-α, β) equals chainBot(α, β).

Русский

Отрицание α меняет роли верхнего и нижнего веса: chainTop(−α, β) = chainBot(α, β).

LaTeX

$$$ \\text{chainTop}(-α, β) = \\text{chainBot}(α, β) $$$

Lean4

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

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

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

Разделы

Аффилиация

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