commShiftIso_zero

Mathlib.CategoryTheory.Shift.CommShift

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.commShiftIso_zero

English

The commShift isomorphism at zero equals the zero-commShift iso for F with respect to A.

Русский

Изоморфизм commShift при нуле равен нулевой коммShift-изоморфизму для F относительно A.

LaTeX

$$$F.commShiftIso 0 = CommShift.isoZero F A$$$

Lean4

theorem commShiftIso_zero : F.commShiftIso (0 : A) = CommShift.isoZero F A :=
  CommShift.zero

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

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

Разделы

Аффилиация

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