Semisimple modules as direct sum of simple modules

Stream: general

[Jesse Vogel]

Suppose I have a semisimple module M. In Lean, is_semisimple_module is defined by the lattice of submodules being a complemented_lattice. The documentation says that "A module is semisimple when every submodule has a complement, or equivalently, the module is a direct sum of simple modules." How do I obtain/formulate this direct sum of simple modules? Is there a function to do so, or how would one implement this? We have been trying to formulate this, but are encountering bundled/unbundled issues..

[Kyle Miller]

Not sure if this helps, but I found docs#complemented_lattice_iff_is_atomistic, which at least gives you that every module is the sum of simple modules