simple_iff_isSimpleModule — Mathlib

English

For a module M over R, Simple(M) in ModuleCat is equivalent to M being a simple R-module.

Русский

Для модуля M над R простота в ModuleCat эквивалентна тому, что M является простым R-модулем.

LaTeX

$$$\mathrm{Simple}(\mathrm{ModuleCat}.of\;R\;M) \iff \mathrm{IsSimpleModule}\;R\;M$$$

Lean4

theorem simple_iff_isSimpleModule : Simple (of R M) ↔ IsSimpleModule R M := by
  rw [simple_iff_subobject_isSimpleOrder, (subobjectModule (of R M)).isSimpleOrder_iff, isSimpleModule_iff]

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