chainBot_zero

Mathlib.Algebra.Lie.Weights.Chain

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

English

The chainBot with zero coefficient is the original weight, i.e., chainBot 0 β = β.

Русский

Нижний вес нулевого коэффициента совпадает с исходным весом: chainBot 0 β = β.

LaTeX

$$$ \\text{chainBot}(0, β) = β $$$

Lean4

@[simp]
theorem chainBot_zero : chainBot 0 β = β := by ext; simp

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

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

Разделы

Аффилиация

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