isotypicComponent

Mathlib.RingTheory.SimpleModule.Isotypic

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

English

IsIsotypic R (isotypicComponent R M S) for any simple S; i.e., an isotypic component is itself isotypic.

Русский

Изотипическая компонента сама по себе является изотипичной.

LaTeX

$$$$ \\mathrm{IsIsotypic}(R, \\mathrm{isotypicComponent}(R,M,S)). $$$$

Lean4

protected theorem isotypicComponent : IsIsotypic R (isotypicComponent R M S) :=
  (IsIsotypicOfType.isotypicComponent R M S).isIsotypic

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

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

Разделы

Аффилиация

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