instAdditiveIntUpSingleFunctor — Mathlib

English

In the up-shift setting, the n-th single functor is additive in the Homotopy category.

Русский

В установке верхнего сдвига, n-й одинарный функтор аддитивен в гомотопической категории.

LaTeX

$$$\forall n,\; (\text{HomotopyCategory.singleFunctor } C n).Additive$$$

Lean4

instance (n : ℤ) : (singleFunctor C n).Additive :=
  by
  dsimp only [singleFunctor, singleFunctors, SingleFunctors.postcomp]
  infer_instance
    -- The object level definitional equality underlying `singleFunctorsPostcompQuotientIso`.

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