Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-22 16:01 f48ce7ec

View on Github →

feat(algebra/lie/basic): define the radical of a Lie algebra and prove it is solvable (#5833)

Estimated changes

Modified src/algebra/lie/basic.lean

added def lie_algebra.radical

modified theorem lie_ideal.derived_series_add_eq_bot

added theorem lie_ideal.of_bot_eq_bot

added theorem lie_ideal.unique_of_bot

modified theorem lie_submodule.coe_to_submodule

modified theorem lie_submodule.coe_to_submodule_eq_iff

modified theorem lie_submodule.ext

modified theorem lie_submodule.mem_carrier

modified theorem lie_submodule.mem_coe

modified theorem lie_submodule.mem_coe_submodule

added theorem lie_submodule.of_bot_eq_bot

added theorem lie_submodule.unique_of_bot

added theorem lie_submodule.zero_mem