Commit 2023-06-12 15:03 df50c172

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/ModuleCat/Simple.lean

added theorem simple_iff_isSimpleModule

added theorem simple_iff_is_simple_module'

added theorem simple_of_finrank_eq_one