of_injective

Mathlib.RingTheory.SimpleModule.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$IsSemisimpleModule R N$$

Lean4

theorem of_injective (f : N →ₗ[R] M) (hf : Function.Injective f) : IsSemisimpleModule R N :=
  congr (Submodule.topEquiv.symm.trans <| Submodule.equivMapOfInjective f hf _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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