Theorems · Theorem · nonassociative algebras

LieAlgebra.IsKilling.eq_zero_of_isNilpotent_ad_of_mem_isCartanSubalgebra

∀ (K : Type u_2) (L : Type u_3) [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L] [FiniteDimensional K L]
  (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] {x : L},
  x ∈ H → IsNilpotent ((LieAlgebra.ad K L) x) → x = 0

If a Lie algebra L has non-degenerate Killing form, the only element of a Cartan subalgebra whose adjoint action on L is nilpotent, is the zero element. Over a perfect field a much stronger result is true, see LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra.

Defined in

Mathlib.Algebra.Lie.Weights.Killing

Cited by

1 results in Mathlib

Foundations

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

Assumes

LieRingFieldLieAlgebraFiniteDimensionalLieSubalgebra.IsCartanSubalgebraLieAlgebra.IsKilling