Commit 2026-04-30 10:17 5d69f04e

View on Github →

feat: Cartan's criterion for semisimplicity (#38749) Cartan's criterion for semisimplicity

Estimated changes

Modified Mathlib/Algebra/Lie/CartanCriterion.lean

added theorem LieAlgebra.hasTrivialRadical_iff_isKilling

added theorem LieAlgebra.isSolvable_of_killingForm_apply_lie_eq_zero

modified theorem LieModule.isNilpotent_derivedSeries_of_traceForm_eq_zero_aux

Modified Mathlib/Algebra/Lie/Killing.lean