ad_nilpotent_of_nilpotent — Mathlib

English

If an element a of a (associative) algebra A is nilpotent, then its adjoint action ad a on A is nilpotent.

Русский

Если элемент a алгебры A нильпотентен, то действие адяда на A, ad a, нильпотентно.

LaTeX

$$IsNilpotent a → IsNilpotent (LieAlgebra.ad R A a)$$

Lean4

theorem _root_.LieAlgebra.ad_nilpotent_of_nilpotent {a : A} (h : IsNilpotent a) : IsNilpotent (LieAlgebra.ad R A a) :=
  by
  rw [LieAlgebra.ad_eq_lmul_left_sub_lmul_right]
  have hl : IsNilpotent (LinearMap.mulLeft R a) := by rwa [LinearMap.isNilpotent_mulLeft_iff]
  have hr : IsNilpotent (LinearMap.mulRight R a) := by rwa [LinearMap.isNilpotent_mulRight_iff]
  have := @LinearMap.commute_mulLeft_right R A _ _ _ _ _ a a
  exact this.isNilpotent_sub hl hr

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