instIsSimpleModule

Mathlib.RingTheory.SimpleModule.Basic

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

English

A ring is semisimple if it is semisimple as a module over itself.

Русский

Кольцо называется семисимплексным, если как модуль над собой оно семисимплексно.

LaTeX

$$$\\text{IsSemisimpleRing}(R) \\;\\equiv\\; \\text{IsSemisimpleModule } R R.$$$

Lean4

instance (R) [DivisionRing R] : IsSimpleModule R R where

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

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

Разделы

Аффилиация

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