mathlib

eccd8dd1 - feat(algebra/lie/nilpotent): generalise lower central series to start with given Lie submodule (#11625)

feat(algebra/lie/nilpotent): generalise lower central series to start with given Lie submodule (#11625) The advantage of this approach is that we can regard the terms of the lower central series of a Lie submodule as Lie submodules of the enclosing Lie module. In particular, this is useful when considering the lower central series of a Lie ideal.