isLieAbelian_iff_center_eq_top — Mathlib

English

A Lie algebra L is abelian if and only if its center is the whole algebra, i.e., IsLieAbelian L ⇔ center R L = ⊤.

Русский

Ли-алгебра L абелева тогда и только тогда, когда ее центр равен всей алгебре: IsLieAbelian L ⇔ center R L = ⊤.

LaTeX

$$$\text{IsLieAbelian } L \;\iff\; \operatorname{center}(R,L) = \top.$$$

Lean4

theorem isLieAbelian_iff_center_eq_top : IsLieAbelian L ↔ center R L = ⊤ :=
  LieModule.isTrivial_iff_max_triv_eq_top R L L

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