isSemisimpleModule_of_surjective

Mathlib.RingTheory.SimpleModule.Basic

URI: https://scilib.ai/kg/mathlib#LinearMap.isSemisimpleModule_of_surjective

English

If each component is semisimple, then the DFinsupp construction is semisimple.

Русский

Если каждая компонента полупрямого модуля полупрямый, то DFinsupp-конструкция полупрямой.

LaTeX

$$IsSemisimpleModule R (DFinsupp fun i => M i)$$

Lean4

axiom _root_.LinearMap.isSemisimpleModule_of_surjective (_ : Function.Surjective l) [IsSemisimpleModule R M'] :
    IsSemisimpleModule S N'

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

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

Разделы

Аффилиация

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