ker — Mathlib

English

Let L be a Lie algebra acting on a Lie module M. The kernel of this action (the set of elements of L acting trivially on all of M) is a Lie ideal of L.

Русский

Пусть Ли-алгебра L действует на модуле М. Дорожка (ядро) этого действия — множество элементов L, действующих тривиально на всем M, является идеалом Ли в L.

LaTeX

$$$K=\\{x\\in L\\mid \\forall m\\in M,\,[x,m]=0\\}$ и $K\\trianglelefteq L$.$$

Lean4

/-- The kernel of the action of a Lie algebra `L` on a Lie module `M` as a Lie ideal in `L`. -/
protected def ker : LieIdeal R L :=
  (toEnd R L M).ker

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