Theorems · Theorem · nonassociative algebras

LieAlgebra.isNilpotent_range_ad_iff

∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieRing.IsNilpotent ↥(LieAlgebra.ad R L).range ↔ LieRing.IsNilpotent L

Note that this result is not quite a special case of LieModule.isNilpotent_range_toEnd_iff which concerns nilpotency of the (ad R L).range-module L, whereas this result concerns nilpotency of the (ad R L).range-module (ad R L).range.

Defined in

Mathlib.Algebra.Lie.Nilpotent

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingLieRingLieAlgebra