instHasZeroObjectOppositeShift

Mathlib.CategoryTheory.Shift.Opposite

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instHasZeroObjectOppositeShift

English

If C has a zero object, then OppositeShift C A has a zero object as well.

Русский

Если у C есть нулевой объект, то и OppositeShift C A имеет нулевой объект.

LaTeX

$$$\text{HasZeroObject}\ (OppositeShift\ C\ A)$ given $\text{HasZeroObject}\ C$ and appropriate shifts.$$

Lean4

instance [HasZeroObject C] : HasZeroObject (OppositeShift C A) :=
  by
  dsimp only [OppositeShift]
  infer_instance

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

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

Разделы

Аффилиация

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