mathlib3

90763c46 - feat(algebra/lie/basic): generalise the definition of `lie_algebra.derived_series` (#5794)

feat(algebra/lie/basic): generalise the definition of `lie_algebra.derived_series` (#5794) This generalisation will make it easier to relate properties of the derived series of a Lie algebra and the derived series of its ideals (regarded as Lie algebras in their own right). The key definition is `lie_algebra.derived_series_of_ideal` and the key result is `lie_ideal.derived_series_eq_bot_iff`.