Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-02-17 07:03
53815d4e
View on Github →
feat: prove isNilpotentAdd for LieSubmodules (
#21962
) Prove isNilpotentAdd for LieSubmodules
Estimated changes
Modified
Mathlib/Algebra/Lie/Nilpotent.lean
added
theorem
LieSubmodule.lowerCentralSeries_eq_bot_iff_lcs_eq_bot: