Commit 2023-09-21 19:02 766dbabf

View on Github →

feat: remove IsNoetherian R L hypothesis from proof that zero-weight space of a Lie module is nilpotent (#7295) This is possible thanks to the commit: 63ca289d983f26977a4c956c729ec33b4e2ad0d6

Estimated changes

Modified Mathlib/Algebra/Lie/Engel.lean

modified theorem LieAlgebra.isEngelian_of_isNoetherian

modified theorem LieAlgebra.isNilpotent_iff_forall

added theorem LieModule.isNilpotent_iff_forall'

modified theorem LieModule.isNilpotent_iff_forall

Modified Mathlib/Algebra/Lie/Weights.lean