instLinearMapIdSubtypeMemSubmoduleOfIsSemisimpleModule_1

Mathlib.RingTheory.SimpleModule.Basic

URI: https://scilib.ai/kg/mathlib#Module.Finite.instLinearMapIdSubtypeMemSubmoduleOfIsSemisimpleModule_1

English

If m is complemented in M, then the space of linear maps from P to m is finite over R₀.

Русский

Если m дополнен в M, то пространство линейных отображений P → m конечномерно над R₀.

LaTeX

$$Module.Finite R₀ (P →ₗ[R] m)$$

Lean4

instance [IsSemisimpleModule R M] : Module.Finite R₀ (P →ₗ[R] m) :=
  .of_isComplemented_codomain _ _ (exists_isCompl m)

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

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

Разделы

Аффилиация

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