isotypicComponents

Mathlib.RingTheory.SimpleModule.Isotypic

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

← MathLib Explorer

English

If m is in isotypicComponents, then m is IsIsotypic.

Русский

Если m лежит в isotypicComponents, то m является IsIsotypic.

LaTeX

$$$$ \\text{If } m \\in \\mathrm{isotypicComponents}(R,M)\\text{ then } \\mathrm{IsIsotypic}(R,m). $$$$

Lean4

protected theorem isotypicComponents {m : Submodule R M} (h : m ∈ isotypicComponents R M) : IsIsotypic R m := by
  obtain ⟨_, _, rfl⟩ := h; exact .isotypicComponent R M _

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

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

Разделы

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

Аффилиация

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