exists_simple_submodule — Mathlib

English

If M is a nontrivial semisimple module over R, then there exists a simple submodule of M.

Русский

Пусть M — не тривиальный полупрямой модуль над R; тогда существует простой подмодуль подмодуля M.

LaTeX

$$(IsSemisimpleModule R M) ∧ (M ≠ 0) ⇒ ∃ m : Submodule R M, IsSimpleModule R m$$

Lean4

theorem exists_simple_submodule [Nontrivial M] : ∃ m : Submodule R M, IsSimpleModule R m := by
  simpa only [isSimpleModule_iff_isAtom] using IsAtomic.exists_atom _

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