Commit 2024-05-31 11:21 5b4a8ff4

View on Github →

feat(Algebra/Lie): Killing Lie algebras are semisimple (#13265)

Estimated changes

Modified Mathlib/Algebra/Lie/Killing.lean

added theorem LieAlgebra.IsKilling.ideal_eq_bot_of_isLieAbelian

Modified Mathlib/Algebra/Lie/TraceForm.lean

added theorem LieModule.traceForm_lieInvariant