Commit 2024-06-09 14:00 491655d4

feat(Algebra, Order): simple submodules in a semisimple module (#13636)

• Add IsAtomic.exists_atom: a nontrivial atomic partial order has an atom, and the dual statement.
• Since the submodule lattice of a semisimple module is atomistic, deduce that every submodule is the sum of its simple submodules, and that any nontrivial submodule has a simple submodule.