instCommShiftTriangleMapTriangleInt

English

There is a canonical commShift structure on the functor mapTriangle, valid for all integers, given by mapTriangleCommShiftIso.

Русский

Существует каноническая структура CommShift на F.mapTriangle для целочисленных сдвигов, задаваемая через mapTriangleCommShiftIso.

LaTeX

$$$\\mathrm{F.mapTriangle}.CommShift(\\mathbb{Z})$ exists with iso $\\mathrm{mapTriangleCommShiftIso}$$$

Lean4

noncomputable instance [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] :
    (F.mapTriangle).CommShift ℤ where
  iso := F.mapTriangleCommShiftIso
  add _ _ := mapTriangleCommShiftIso_add ..

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