Theorem simple_iff_isSimpleModule

Modification history

2025-08-13 09:52

Mathlib/Algebra/Category/ModuleCat/Simple.lean

chore(RingTheory): use `extend` instead of `abbrev` in `IsS(emis)impleModule` (#27427)

Modified simple_iff_isSimpleModule View on Github →

2023-06-12 15:03

Mathlib/Algebra/Category/ModuleCat/Simple.lean

feat: port Algebra.Category.Module.Simple (#4992)

Added simple_iff_isSimpleModule View on Github →