Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-10 10:46 04909776

View on Github →

feat(algebra/lie/engel): add proof of Engel's theorem (#11922)

Estimated changes

Modified docs/references.bib

Modified src/algebra/lie/cartan_subalgebra.lean

added theorem lie_subalgebra.lie_mem_sup_of_mem_normalizer

Created src/algebra/lie/engel.lean

added theorem function.surjective.is_engelian

added theorem lie_algebra.exists_engelian_lie_subalgebra_of_lt_normalizer

added def lie_algebra.is_engelian

added theorem lie_algebra.is_engelian_of_is_noetherian

added theorem lie_algebra.is_engelian_of_subsingleton

added theorem lie_algebra.is_nilpotent_iff_forall

added theorem lie_equiv.is_engelian_iff

added theorem lie_module.is_nilpotent_iff_forall

added theorem lie_submodule.exists_smul_add_of_span_sup_eq_top

added theorem lie_submodule.is_nilpotent_of_is_nilpotent_span_sup_eq_top

added theorem lie_submodule.lcs_le_lcs_of_is_nilpotent_span_sup_eq_top

added theorem lie_submodule.lie_top_eq_of_span_sup_eq_top

Modified src/algebra/lie/of_associative.lean

added theorem lie_subalgebra.to_endomorphism_eq

added theorem lie_subalgebra.to_endomorphism_mk

added theorem lie_submodule.coe_map_to_endomorphism_le

Modified src/algebra/lie/subalgebra.lean

added theorem lie_subalgebra.subsingleton_bot

Modified src/algebra/module/submodule.lean

added theorem submodule.injective_subtype

Modified src/linear_algebra/basic.lean

added theorem submodule.span_sup

added theorem submodule.sup_span