Commit 2024-05-28 14:16 161b8412

View on Github →

feat(Algebra/Lie/Semisimple): API for semisimple Lie algebras (#13217) Including the result that ideals in a semisimple Lie algebra are in a unique way the direct sum of simple ideals. This result makes no assumptions on the ring of coefficients or the Lie algebra; it holds over arbitrary base rings, and in arbitrary dimensions.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Lie/Derivation/Killing.lean

Modified Mathlib/Algebra/Lie/Semisimple.lean

added theorem LieAlgebra.HasTrivialRadical.center_eq_bot

added theorem LieAlgebra.IsSemisimple.booleanGenerators

added theorem LieAlgebra.IsSemisimple.finitelyAtomistic

added theorem LieAlgebra.IsSemisimple.isSimple_of_isAtom

added theorem LieAlgebra.IsSimple.eq_top_of_isAtom

added theorem LieAlgebra.IsSimple.isAtom_iff_eq_top

added theorem LieAlgebra.IsSimple.isAtom_top

deleted theorem LieAlgebra.center_eq_bot_of_hasTrivialRadical

Modified Mathlib/Order/BooleanAlgebra.lean

added def DistribLattice.booleanAlgebraOfComplemented

Created Mathlib/Order/BooleanGenerators.lean

added theorem IsCompactlyGenerated.BooleanGenerators.atomistic

added def IsCompactlyGenerated.BooleanGenerators.booleanAlgebra_of_sSup_eq_top

added theorem IsCompactlyGenerated.BooleanGenerators.complementedLattice_of_sSup_eq_top

added def IsCompactlyGenerated.BooleanGenerators.distribLattice_of_sSup_eq_top

added theorem IsCompactlyGenerated.BooleanGenerators.eq_atoms_of_sSup_eq_top

added theorem IsCompactlyGenerated.BooleanGenerators.isAtomistic_of_sSup_eq_top

added theorem IsCompactlyGenerated.BooleanGenerators.mem_of_isAtom_of_le_sSup_atoms

added theorem IsCompactlyGenerated.BooleanGenerators.mono

added theorem IsCompactlyGenerated.BooleanGenerators.sSup_inter

added theorem IsCompactlyGenerated.BooleanGenerators.sSup_le_sSup_iff_of_atoms

added structure IsCompactlyGenerated.BooleanGenerators

Modified Mathlib/Order/SupIndep.lean

added theorem CompleteLattice.setIndependent_singleton