Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-16 07:31 47b3c4b4

View on Github →

feat(algebra/lie/basic): nilpotent and solvable Lie algebras (#5382)

Estimated changes

Modified src/algebra/lie/basic.lean

deleted def derived_lie_ideal

deleted def derived_lie_submodule

added def lie_algebra.derived_series

added theorem lie_module.derived_series_le_lower_central_series

added def lie_module.lower_central_series

added theorem lie_module.trivial_iff_derived_eq_bot

added theorem lie_submodule.trivial_lie_oper_zero

deleted theorem trivial_iff_derived_eq_bot

added theorem trivial_lie_zero