IsIsotypic

Mathlib.RingTheory.SimpleModule.Isotypic

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

← MathLib Explorer

English

If M is a subsingleton, then IsIsotypic R M holds for any S.

Русский

Если M состоит из одного элемента (subsingleton), то IsIsotypic верно для любого S.

LaTeX

$$$[Subsingleton M] \\Rightarrow IsIsotypic R M.$$

Lean4

/-- An `R`-module `M` is isotypic if all its simple submodules are isomorphic. -/
def IsIsotypic : Prop :=
  ∀ (m : Submodule R M) [IsSimpleModule R m], IsIsotypicOfType R M m

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

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

Разделы

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

Аффилиация

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