Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-08 12:10 65fba4cb

View on Github →

feat(algebra/lie/centralizer): define the centralizer of a Lie submodule and the upper central series (#14173)

Estimated changes

Modified src/algebra/lie/cartan_subalgebra.lean

deleted theorem lie_subalgebra.exists_nested_lie_ideal_of_le_normalizer

deleted theorem lie_subalgebra.ideal_in_normalizer

deleted theorem lie_subalgebra.le_normalizer

deleted theorem lie_subalgebra.le_normalizer_of_ideal

deleted theorem lie_subalgebra.lie_mem_sup_of_mem_normalizer

deleted theorem lie_subalgebra.mem_normalizer_iff'

deleted theorem lie_subalgebra.mem_normalizer_iff

deleted def lie_subalgebra.normalizer

deleted theorem lie_subalgebra.normalizer_eq_self_iff

Created src/algebra/lie/centralizer.lean

added theorem lie_subalgebra.coe_centralizer_eq_normalizer

added theorem lie_subalgebra.exists_nested_lie_ideal_of_le_normalizer

added theorem lie_subalgebra.ideal_in_normalizer

added theorem lie_subalgebra.le_normalizer

added theorem lie_subalgebra.lie_mem_sup_of_mem_normalizer

added theorem lie_subalgebra.mem_normalizer_iff'

added theorem lie_subalgebra.mem_normalizer_iff

added def lie_subalgebra.normalizer

added theorem lie_subalgebra.normalizer_eq_self_iff

added def lie_submodule.centralizer

added theorem lie_submodule.centralizer_bot_eq_max_triv_submodule

added theorem lie_submodule.centralizer_inf

added theorem lie_submodule.comap_centralizer

added theorem lie_submodule.gc_top_lie_centralizer

added theorem lie_submodule.le_centralizer

added theorem lie_submodule.mem_centralizer

added theorem lie_submodule.monotone_centalizer

added theorem lie_submodule.top_lie_le_iff_le_centralizer

Modified src/algebra/lie/engel.lean

Modified src/algebra/lie/ideal_operations.lean

added theorem lie_submodule.lie_le_iff

Modified src/algebra/lie/nilpotent.lean

added theorem lie_module.is_nilpotent_iff

added theorem lie_module.is_nilpotent_iff_exists_ucs_eq_top

added theorem lie_submodule.gc_lcs_ucs

added theorem lie_submodule.is_nilpotent_iff_exists_self_le_ucs

added theorem lie_submodule.lcs_add_le_iff

added theorem lie_submodule.lcs_le_iff

added def lie_submodule.ucs

added theorem lie_submodule.ucs_comap_incl

added theorem lie_submodule.ucs_eq_self_of_centralizer_eq_self

added theorem lie_submodule.ucs_eq_top_iff

added theorem lie_submodule.ucs_le_of_centralizer_eq_self

added theorem lie_submodule.ucs_mono

added theorem lie_submodule.ucs_succ

added theorem lie_submodule.ucs_zero

Modified src/algebra/lie/submodule.lean

added theorem lie_submodule.comap_incl_eq_top