Simple objects in the category of R
-modules #
We prove simple modules are exactly simple objects in the category of R
-modules.
theorem
simple_iff_is_simple_module
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M] :
category_theory.simple (Module.of R M) ↔ is_simple_module R M
@[protected, instance]
def
simple_of_is_simple_module
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
[is_simple_module R M] :
A simple module is a simple object in the category of modules.
@[protected, instance]
A simple object in the category of modules is a simple module.