Theorem simple_iff_is_simple_module'

Modification history

2023-06-16 02:09
Mathlib/Algebra/Category/ModuleCat/Simple.lean
chore: tidy various files (#5104)
Deleted simple_iff_is_simple_module'View on Github →
2023-06-12 15:03
Mathlib/Algebra/Category/ModuleCat/Simple.lean
feat: port Algebra.Category.Module.Simple (#4992)
Added simple_iff_is_simple_module'View on Github →