instIsSemisimpleRing

Mathlib.RingTheory.SimpleModule.WedderburnArtin

URI: https://scilib.ai/kg/mathlib#IsSimpleRing.instIsSemisimpleRing

English

The instance provides that a simple Artinian ring is semisimple.

Русский

Экземпляр обеспечивает, что простое артинское кольцо является полупрямым.

LaTeX

$$IsSimpleRing R ⇒ IsSemisimpleRing R$$

Lean4

instance (priority := low) : IsSemisimpleRing R :=
  (isSimpleRing_isArtinianRing_iff.mp ⟨‹_›, ‹_›⟩).1

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

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

Разделы

Аффилиация

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