Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-19 13:11 90763c46

View on Github →

feat(algebra/lie/basic): generalise the definition of lie_algebra.derived_series (#5794) This generalisation will make it easier to relate properties of the derived series of a Lie algebra and the derived series of its ideals (regarded as Lie algebras in their own right). The key definition is lie_algebra.derived_series_of_ideal and the key result is lie_ideal.derived_series_eq_bot_iff.

Estimated changes

added theorem lie_algebra.map_zero
modified theorem lie_ideal.comap_mono
modified theorem lie_ideal.map_mono
added theorem lie_subalgebra.add_mem
modified theorem lie_subalgebra.coe_bracket
added theorem lie_subalgebra.lie_mem
modified theorem lie_subalgebra.mem_coe'
modified theorem lie_subalgebra.mem_coe
added theorem lie_subalgebra.mk_coe