chainLength_of_isZero

Mathlib.Algebra.Lie.Weights.RootSystem

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

English

If α is zero, then the chain length is zero in the IsKilling setting.

Русский

Если α равно нулю, то длина цепи равна нулю в настройке IsKilling.

LaTeX

$$$\\text{If } α^0,\\; \\mathrm{chainLength}(α,β)=0.$$$

Lean4

theorem chainLength_of_isZero (hα : α.IsZero) : chainLength α β = 0 :=
  dif_pos hα

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

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

Разделы

Аффилиация

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