instIsSemisimpleModuleOfIsSimpleModule

Mathlib.RingTheory.SimpleModule.Basic

URI: https://scilib.ai/kg/mathlib#instIsSemisimpleModuleOfIsSimpleModule

English

If R is a division ring, then R is a simple module over itself.

Русский

Если R — делительный кольцо, то R является простым модулем над собой.

LaTeX

$$$R\\text{ прост как левый }R\\text{-модуль} \\iff \\text{IsSimpleModule } R R$.$$

Lean4

instance [IsSimpleModule R M] : IsSemisimpleModule R M where

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

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

Разделы

Аффилиация

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