We discuss the theory of Lie algebras in Lean's Mathlib library. Using nilpotency as the theme, we outline a computer formalisation of Engel's theorem and an application to root space theory. We emphasise that all arguments work with coefficients in any commutative ring.

翻译：我们在Lean的Mathlib库中讨论李代数理论。以零幂性为主题，我们概述了Engel定理的计算机化表述及其在根空间理论中的应用。我们强调所有论证在任何可交换环上的系数都成立。