self_module_ker_eq_center — Mathlib

English

For a Lie algebra L over R, the kernel of the self-action LieModule.ker R L L equals the center of L; in other words, LieModule.ker R L L = center R L.

Русский

Для Ли-алгебры L над R ядро собственного действия совпадает с центром L; то есть LieModule.ker R L L = center R L.

LaTeX

$$$\operatorname{LieModule.ker}\;R\;L\;L = \operatorname{center}(R,L).$$$

Lean4

@[simp]
theorem self_module_ker_eq_center : LieModule.ker R L L = center R L :=
  by
  ext y
  simp only [LieModule.mem_maxTrivSubmodule, LieModule.mem_ker, ← lie_skew _ y, neg_eq_zero]

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