Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-24 16:03 eccd8dd1

View on Github →

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.

Estimated changes