mathlib documentation

algebra.category.Module.simple

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] :
@[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.