Theorem LieAlgebra.ad_mem_adjoin_of_isNilpotent

Modification history

2026-04-21 14:07
Mathlib/Algebra/Lie/AdjointAction/JordanChevalley.lean
feat: a Lie module with trivial trace form is nilpotent over the derived subalgebra (#37622) …
Added LieAlgebra.ad_mem_adjoin_of_isNilpotentView on Github →