projective_of_isSemisimpleRing

Mathlib.RingTheory.SimpleModule.InjectiveProjective

URI: https://scilib.ai/kg/mathlib#Module.projective_of_isSemisimpleRing

English

If R is semisimple, then any R-module M is projective.

Русский

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

LaTeX

$$Module.Projective R M.$$

Lean4

theorem projective_of_isSemisimpleRing : Module.Projective R M :=
  .of_lifting_property'' (IsSemisimpleModule.lifting_property · · _)

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

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

Разделы

Аффилиация

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