mathlib3 documentation

algebra.category.Module.simple

Simple objects in the category of R-modules #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We prove simple modules are exactly simple objects in the category of R-modules.

@[protected, instance]

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.

theorem simple_of_finrank_eq_one {R : Type u_1} [ring R] {k : Type u_2} [field k] [algebra k R] {V : Module R} (h : finite_dimensional.finrank k V = 1) :

Any k-algebra module which is 1-dimensional over k is simple.