chainBotCoeff_zero

Mathlib.Algebra.Lie.Weights.Chain

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

English

Bot coefficient at zero equals zero: chainBotCoeff 0 β = 0.

Русский

Нижний коэффициент при нуле равен нулю: chainBotCoeff 0 β = 0.

LaTeX

$$$\operatorname{chainBotCoeff} \, 0 \; β = 0$$$

Lean4

@[simp]
theorem chainBotCoeff_zero : chainBotCoeff 0 β = 0 :=
  dif_pos neg_zero

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

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

Разделы

Аффилиация

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