Commit 2024-06-09 14:00 491655d4

View on Github →

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.

Estimated changes