chainLength_zero

Mathlib.Algebra.Lie.Weights.RootSystem

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

English

For nontrivial L, chainLength α 0 equals 2, i.e., the chain through zero has fixed length 2 when α is nonzero.

Русский

Для нетривиального L, chainLength α 0 равно 2, если α ненулевой.

LaTeX

$$$\operatorname{chainLength}(\alpha, 0) = 2$$$

Lean4

@[simp]
theorem chainLength_zero [Nontrivial L] : chainLength 0 β = 0 := by simp [← chainBotCoeff_add_chainTopCoeff]

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

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

Разделы

Аффилиация

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