chainTopCoeff_neg

Mathlib.Algebra.Lie.Weights.Chain

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

English

There is a symmetry relating chainTopCoeff and chainBotCoeff: chainBotCoeff(−α) β = chainTopCoeff α β.

Русский

Симметрия между chainTopCoeff и chainBotCoeff: chainBotCoeff(−α) β = chainTopCoeff α β.

LaTeX

$$$\operatorname{chainBotCoeff}( -α ) β = \operatorname{chainTopCoeff}( α ) β$$$

Lean4

@[simp]
theorem chainTopCoeff_neg : chainTopCoeff (-α) β = chainBotCoeff α β :=
  rfl

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

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

Разделы

Аффилиация

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