Theorem LieModule.isNilpotent_derivedSeries_of_traceForm_eq_zero_aux

Modification history

2026-04-30 10:17
Mathlib/Algebra/Lie/CartanCriterion.lean
feat: Cartan's criterion for semisimplicity (#38749) …
Modified LieModule.isNilpotent_derivedSeries_of_traceForm_eq_zero_auxView on Github →
2026-04-29 11:39
Mathlib/Algebra/Lie/CartanCriterion.lean
feat: drop IsAlgClosed hypothesis from isNilpotent_derivedSeries_of_traceForm_eq_zero_algClosed (#38542) …
Added LieModule.isNilpotent_derivedSeries_of_traceForm_eq_zero_auxView on Github →