Theorems · Theorem · nonassociative algebras

LieAlgebra.ad_mem_adjoin_of_isNilpotent

∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [PerfectField K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [FiniteDimensional K V] {n s : Module.End K V},
  Commute n s →
    IsNilpotent n →
      s.IsSemisimple → (LieAlgebra.ad K (Module.End K V)) n ∈ K[(LieAlgebra.ad K (Module.End K V)) (n + s)]

The adjoint of the nilpotent part of a JC decomposition lies in the subalgebra generated by the adjoint of the sum.

Defined in

Mathlib.Algebra.Lie.AdjointAction.JordanChevalley

Cited by

0 results in Mathlib

Foundations

Depth 135 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldPerfectFieldAddCommGroupModuleFiniteDimensional