nilpotent_ad_of_nilpotent_algebra

English

If an algebra is nilpotent, then its adjoint representation on itself is nilpotent; equivalently, each ad x is nilpotent.

Русский

Если алгебра нильпотентна, то ее представление ад-оператора на самой себе нильпотентно; то есть каждый ad x нильпотент.

LaTeX

$$[IsNilpotent L] ⇒ ∃ k, ∀ x ∈ L, ad_R L x ^ k = 0$$

Lean4

theorem nilpotent_ad_of_nilpotent_algebra [IsNilpotent L] : ∃ k : ℕ, ∀ x : L, ad R L x ^ k = 0 :=
  LieModule.exists_forall_pow_toEnd_eq_zero R L L

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