mathlib

ee4be2db - feat(ring_theory/simple_module): Simple modules as simple objects in the Module category (#11927)

feat(ring_theory/simple_module): Simple modules as simple objects in the Module category (#11927) A simple module is a simple object in the Module category. From there it should be easy to write an alternative proof of Schur's lemma for modules using category theory (using the work already done in category_theory/preadditive/schur.lean). The other direction (a simple object in the Module category is a simple module) hasn't been proved yet. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: pbazin <75327486+pbazin@users.noreply.github.com>