of_subsingleton

Mathlib.RingTheory.SimpleModule.Isotypic

URI: https://scilib.ai/kg/mathlib#IsIsotypicOfType.of_subsingleton

← MathLib Explorer

English

If M is a subsingleton, then IsIsotypic R M holds.

Русский

Если M — субодиночное множество, то IsIsotypic верно.

LaTeX

$$[Subsingleton M] ⇒ IsIsotypic R M.$$

Lean4

@[nontriviality]
theorem of_subsingleton [Subsingleton M] : IsIsotypicOfType R M S := fun S ↦
  have := IsSimpleModule.nontrivial R S
  (not_subsingleton _ S.subtype_injective.subsingleton).elim

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

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

Разделы

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

Аффилиация

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