instIsSemisimpleModuleSubtypeMemSubmoduleValSetIsotypicComponents

Mathlib.RingTheory.SimpleModule.Isotypic

URI: https://scilib.ai/kg/mathlib#instIsSemisimpleModuleSubtypeMemSubmoduleValSetIsotypicComponents

English

If S is simple and c is an isotypic component, then c is semisimple as an R-module.

Русский

Если S прост, то изотипическая компонента c является семисимплексным по модулю R.

LaTeX

$$$IsSemisimpleModule(R, c)$$$

Lean4

instance (c : isotypicComponents R M) : IsSemisimpleModule R c := by obtain ⟨c, S, _, rfl⟩ := c; infer_instance

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

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

Разделы

Аффилиация

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