sSup_simples_eq_top_iff_isSemisimpleModule

English

A module is semisimple iff it is generated by its simple submodules.

Русский

Модуль полупрямой тогда и только тогда, когда он порожден своими простыми подмодулями.

LaTeX

$$sSup {m : Submodule R M | IsSimpleModule R m} = ⊤ ↔ IsSemisimpleModule R M$$

Lean4

/-- A module is semisimple iff it is generated by its simple submodules. -/
theorem sSup_simples_eq_top_iff_isSemisimpleModule :
    sSup {m : Submodule R M | IsSimpleModule R m} = ⊤ ↔ IsSemisimpleModule R M :=
  ⟨.of_sSup_simples_eq_top, fun _ ↦ IsSemisimpleModule.sSup_simples_eq_top _ _⟩

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