Commit 2023-06-12 09:47 eba2601f

View on Github →

feat: port Algebra.Lie.Engel (#4926)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/Engel.lean

added theorem Function.Surjective.isEngelian

added def LieAlgebra.IsEngelian

added theorem LieAlgebra.exists_engelian_lieSubalgebra_of_lt_normalizer

added theorem LieAlgebra.isEngelian_of_isNoetherian

added theorem LieAlgebra.isEngelian_of_subsingleton

added theorem LieAlgebra.isNilpotent_iff_forall

added theorem LieEquiv.isEngelian_iff

added theorem LieModule.isNilpotent_iff_forall

added theorem LieSubmodule.exists_smul_add_of_span_sup_eq_top

added theorem LieSubmodule.isNilpotentOfIsNilpotentSpanSupEqTop

added theorem LieSubmodule.lcs_le_lcs_of_is_nilpotent_span_sup_eq_top

added theorem LieSubmodule.lie_top_eq_of_span_sup_eq_top