simple_of_isSimpleModule — Mathlib

English

If M is an IsSimpleModule over R, then the corresponding ModuleCat object is Simple.

Русский

Если M является простым R-модулем, то соответствующий объект в ModuleCat прост.

LaTeX

$$$[IsSimpleModule\;R\;M] \Rightarrow \mathrm{Simple}(\mathrm{ModuleCat}.of\;R\;M)$$$

Lean4

/-- A simple module is a simple object in the category of modules. -/
instance simple_of_isSimpleModule [IsSimpleModule R M] : Simple (of R M) :=
  simple_iff_isSimpleModule.mpr ‹_›

Похожие утверждения