mathlib

07a1b8db - feat(ring_theory/simple_module): introduce `is_semisimple_module` (#6215)

feat(ring_theory/simple_module): introduce `is_semisimple_module` (#6215) Defines `is_semisimple_module` to mean that the lattice of submodules is complemented Shows that this is equivalent to the module being the `Sup` of its simple submodules