Commit 2024-02-03 07:19 a0cb47af

View on Github →

feat(Algebra/Lie): Engel subalgebras (#10158) Progress toward https://github.com/leanprover-community/mathlib4/issues/10065

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/EngelSubalgebra.lean

added def LieSubalgebra.engel

added theorem LieSubalgebra.isNilpotent_of_forall_le_engel

added theorem LieSubalgebra.mem_engel_iff

added theorem LieSubalgebra.normalizer_engel

added theorem LieSubalgebra.normalizer_eq_self_of_engel_le

added theorem LieSubalgebra.self_mem_engel

Modified Mathlib/Algebra/Lie/OfAssociative.lean

added theorem LieAlgebra.ad_lie

added theorem LieAlgebra.ad_pow_lie

added theorem LieModule.toEndomorphism_lie

added theorem LieModule.toEndomorphism_pow_lie

added theorem LieSubalgebra.coe_ad

added theorem LieSubalgebra.coe_ad_pow

added theorem LieSubmodule.coe_toEndomorphism

added theorem LieSubmodule.coe_toEndomorphism_pow