instIsLieAbelianSubtypeMemLieSubmoduleCenter

Mathlib.Algebra.Lie.Abelian

URI: https://scilib.ai/kg/mathlib#LieAlgebra.instIsLieAbelianSubtypeMemLieSubmoduleCenter

English

The center of a Lie algebra L is an abelian Lie algebra.

Русский

Центр Ли-алгебры L является абелевой Ли-алгеброй.

LaTeX

$$$\\operatorname{center}(R,L)$ is abelian: $\\forall x,y\\in \\operatorname{center}(R,L),\\,[x,y]=0$.$$

Lean4

instance : IsLieAbelian (center R L) :=
  inferInstance

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

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

Разделы

Аффилиация

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