submodule

Mathlib.RingTheory.SimpleModule.Basic

URI: https://scilib.ai/kg/mathlib#IsSemisimpleModule.submodule

← MathLib Explorer

English

Any submodule m of a semisimple R-module M is itself semisimple.

Русский

Любой подмодуль m полупрямого R-модуля M сам является полупрямым.

LaTeX

$$IsSemisimpleModule R m$$

Lean4

instance submodule {m : Submodule R M} : IsSemisimpleModule R m where
  __ := m.mapIic.complementedLattice_iff.2 IsModularLattice.complementedLattice_Iic

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru