instAdditiveModuleCatObjFunctorCoinvariantsTensor

Mathlib.RepresentationTheory.Coinvariants

URI: https://scilib.ai/kg/mathlib#Rep.instAdditiveModuleCatObjFunctorCoinvariantsTensor

English

The object ((coinvariantsTensor k G).obj A) carries a natural additive structure.

Русский

Объект ((coinvariantsTensor k G).obj A) естественно предствлен как аддитивное объект в категории модулей.

LaTeX

$$(((coinvariantsTensor k G).obj A).Additive)$$

Lean4

instance (A : Rep k G) : ((coinvariantsTensor k G).obj A).Additive where

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

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

Разделы

Аффилиация

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