lie_zero

Mathlib.Algebra.Lie.Basic

URI: https://scilib.ai/kg/mathlib#lie_zero

English

Another instance of Lie algebra L acting on itself by bracket, i.e., adjoint action.

Русский

Еще один экземпляр действия Ли над собой через скобку.

LaTeX

$$$\\text{LieModule } R\\; L\\; L$$$

Lean4

@[simp]
theorem lie_zero : ⁅x, 0⁆ = (0 : M) :=
  (AddMonoidHom.mk' _ (lie_add x)).map_zero

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

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

Разделы

Аффилиация

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