ad_ker_eq_center — Mathlib

English

Another form: the set membership in idealRange corresponds to existence of a preimage under ad.

Русский

Ещё одно: принадлежность в идеальном диапазоне соответствует существованию предобразного элемента под ad.

LaTeX

$$$D\\in (ad\\,R\\,L).idealRange\\iff \\exists x:\\, L,\\; ad\\,R\\,L\\; x = D$$$

Lean4

/-- The kernel of the adjoint action on a Lie algebra is equal to its center. -/
theorem ad_ker_eq_center : (ad R L).ker = LieAlgebra.center R L :=
  by
  ext x
  rw [← LieAlgebra.self_module_ker_eq_center, LieHom.mem_ker, LieModule.mem_ker]
  simp [DFunLike.ext_iff]

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