res_additive

Mathlib.CategoryTheory.Action.Limits

URI: https://scilib.ai/kg/mathlib#Action.res_additive

English

Restriction functor res V f along a monoid hom f : G →* H is additive.

Русский

Функтор ограничения res V f по гомоморфизму моноида f: G →* H аддитивен.

LaTeX

$$$\text{res}(V,f).\mathrm{Additive}$$$

Lean4

instance res_additive : (res V f).Additive where

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

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

Разделы

Аффилиация

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