mathlib

f7c1e5f2 - feat(algebra/lie/nilpotent): basic lemmas about nilpotency for Lie subalgebras of associative algebras (#8090)

feat(algebra/lie/nilpotent): basic lemmas about nilpotency for Lie subalgebras of associative algebras (#8090) The main lemma is: `lie_algebra.is_nilpotent_ad_of_is_nilpotent` which is the first step in proving Engel's theorem. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>