quotient

Mathlib.RingTheory.SimpleModule.Basic

URI: https://scilib.ai/kg/mathlib#IsSemisimpleModule.quotient

English

If f: M → N is surjective and M is semisimple, then N is semisimple.

Русский

Если отображение f: M → N сюръективно и M полупрямый, то N полупрямый.

LaTeX

$$IsSemisimpleModule R N$$

Lean4

instance quotient : IsSemisimpleModule R (M ⧸ m) :=
  have ⟨P, compl⟩ := exists_isCompl m
  .congr (m.quotientEquivOfIsCompl P compl)

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

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

Разделы

Аффилиация

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