chainBotCoeff_zero_right

Mathlib.Algebra.Lie.Weights.RootSystem

URI: https://scilib.ai/kg/mathlib#LieAlgebra.IsKilling.chainBotCoeff_zero_right

English

Similarly, chainBotCoeff α 0 equals 1 in the nontrivial case.

Русский

Аналогично, chainBotCoeff α 0 = 1 в нетривиальном случае.

LaTeX

$$$\operatorname{chainBotCoeff}(α,0) = 1$$$

Lean4

theorem chainBotCoeff_zero_right [Nontrivial L] (hα : α.IsNonZero) : chainBotCoeff α (0 : Weight K H L) = 1 :=
  chainTopCoeff_zero_right (-α) hα.neg

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

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

Разделы

Аффилиация

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