Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-23 17:14 59bf982e

View on Github →

feat(algebra/lie/nilpotent): basic facts about nilpotent Lie algebras (#6378)

Estimated changes

Modified src/algebra/lie/ideal_operations.lean

added theorem lie_ideal.map_bracket_eq

Modified src/algebra/lie/nilpotent.lean

added theorem function.injective.lie_algebra_is_nilpotent

added theorem function.surjective.lie_algebra_is_nilpotent

added def lie_algebra.is_nilpotent

added theorem lie_algebra.nilpotent_iff_equiv_nilpotent

added theorem lie_ideal.lower_central_series_map_eq

added theorem lie_ideal.lower_central_series_map_le

Modified src/algebra/lie/subalgebra.lean

added theorem lie_subalgebra.sub_mem

Modified src/algebra/lie/submodule.lean

added theorem lie_hom.ideal_range_eq_top_of_surjective

added theorem lie_hom.is_ideal_morphism_of_surjective

added theorem lie_hom.range_coe_submodule

added theorem lie_hom.range_eq_top

added theorem lie_ideal.coe_map_of_surjective

modified theorem lie_ideal.map_sup_ker_eq_map

added theorem lie_ideal.mem_map_of_surjective

added theorem lie_ideal.top_coe_lie_subalgebra