unopFunctor_additive

Mathlib.Algebra.Homology.Opposite

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.unopFunctor_additive

English

The unop functor is additive in a preadditive setting.

Русский

Обратный функтор (unop) является аддитивным в условиях предадитивности.

LaTeX

$$(@unopFunctor ι V _ c _).Additive$$

Lean4

instance unopFunctor_additive : (@unopFunctor ι V _ c _).Additive where

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

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

Разделы

Аффилиация

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