Commit 2023-06-05 10:52 11c160d2

View on Github →

feat: port Algebra.Lie.Semisimple (#4680)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/Semisimple.lean

added theorem LieAlgebra.abelian_radical_iff_solvable_is_abelian

added theorem LieAlgebra.abelian_radical_of_semisimple

added theorem LieAlgebra.ad_ker_eq_bot_of_semisimple

added theorem LieAlgebra.center_eq_bot_of_semisimple

added theorem LieAlgebra.isSemisimple_iff_no_abelian_ideals

added theorem LieAlgebra.isSemisimple_iff_no_solvable_ideals

added theorem LieAlgebra.subsingleton_of_semisimple_lie_abelian