instAdditiveIntFunctorSingleFunctors

Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors

URI: https://scilib.ai/kg/mathlib#CochainComplex.instAdditiveIntFunctorSingleFunctors

English

For any integer n, the n-th single functor (CochainComplex) is additive.

Русский

Для любого целого n н-й одинарный функционал (CochainComplex) взаимно аддитивен.

LaTeX

$$$\forall n\in\mathbb{Z},\; (\text{CochainComplex.singleFunctors C}).functor(n).Additive$$$

Lean4

instance (n : ℤ) : ((singleFunctors C).functor n).Additive :=
  by
  dsimp only [singleFunctors]
  infer_instance

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

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

Разделы

Аффилиация

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