Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-04 21:44 ee4be2db

View on Github →

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.

Estimated changes