Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-21 14:01 b52b3041

View on Github →

feat(algebra/lie/basic): show I + J is solvable if Lie ideals I, J are solvable (#5819) The key result is lie_algebra.is_solvable_add

Estimated changes

Modified src/algebra/lie/basic.lean

modified def lie_algebra.derived_series

modified def lie_algebra.derived_series_of_ideal

modified theorem lie_algebra.derived_series_of_ideal_add

added theorem lie_algebra.derived_series_of_ideal_add_le_add

modified theorem lie_algebra.derived_series_of_ideal_antimono

modified theorem lie_algebra.derived_series_of_ideal_le_self

modified theorem lie_algebra.derived_series_of_ideal_mono

modified theorem lie_algebra.derived_series_of_ideal_succ_le

added theorem lie_ideal.derived_series_add_eq_bot

modified def lie_module.lower_central_series

added theorem lie_module.lower_central_series_succ

added theorem lie_module.lower_central_series_zero

Modified src/order/preorder_hom.lean

added theorem preorder_hom.iterate_sup_le_sup_iff