isSemisimpleRing_of_isReduced

Mathlib.RingTheory.Artinian.Module

URI: https://scilib.ai/kg/mathlib#IsArtinianRing.isSemisimpleRing_of_isReduced

English

If R is reduced and Artinian, then R is semisimple.

Русский

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

LaTeX

$$$[\text{IsReduced}(R)] \land [IsArtinianRing(R)] \Rightarrow \mathrm{IsSemisimpleRing}(R)$$$

Lean4

theorem isSemisimpleRing_of_isReduced [IsReduced R] : IsSemisimpleRing R :=
  (equivPi R).symm.isSemisimpleRing

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

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

Разделы

Аффилиация

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