abelian_of_le_center — Mathlib

English

If I is a LieIdeal of L and I is contained in the center of L, then I is LieAbelian; i.e., [x,y] = 0 for all x,y ∈ I.

Русский

Если I — либ-идеал Ли L и I ⊆ центр L, то I абелево относительно данной операции: [x,y] = 0 для всех x,y ∈ I.

LaTeX

$$$I \le \mathrm{center}(R,L) \Rightarrow \; \text{IsLieAbelian}(I).$$$

Lean4

theorem abelian_of_le_center (I : LieIdeal R L) (h : I ≤ center R L) : IsLieAbelian I :=
  haveI : LieModule.IsTrivial L I := (LieModule.trivial_iff_le_maximal_trivial R L L I).mpr h
  LieIdeal.isLieAbelian_of_trivial R L I

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