of_mem_isotypicComponents

Mathlib.RingTheory.SimpleModule.Isotypic

URI: https://scilib.ai/kg/mathlib#Submodule.IsFullyInvariant.of_mem_isotypicComponents

← MathLib Explorer

English

If m ∈ isotypicComponents(R,M) then m is fully invariant.

Русский

Если m принадлежит isotypicComponents(R,M), то m полностью инвариантен.

LaTeX

$$$$ m \\in \\mathrm{isotypicComponents}(R,M) \\Rightarrow m.\\mathrm{IsFullyInvariant}. $$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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