isNilpotent_ad_of_isNilpotent — Mathlib

English

If x ∈ a Lie subalgebra L of A has nilpotent adjoint action ad_R L x, then ad_R A x is nilpotent as a Lie algebra endomorphism.

Русский

Если x ∈ L ⊆ A имеет нильпотентное действие ад, то ad_A x нильпотентно на A.

LaTeX

$$IsNilpotent (ad R L x) → IsNilpotent (LieHom.instFunLike.coe (LieAlgebra.ad R A) x)$$

Lean4

theorem _root_.LieAlgebra.isNilpotent_ad_of_isNilpotent {L : LieSubalgebra R A} {x : L} (h : IsNilpotent (x : A)) :
    IsNilpotent (LieAlgebra.ad R L x) :=
  L.isNilpotent_ad_of_isNilpotent_ad <| LieAlgebra.ad_nilpotent_of_nilpotent R h

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