shift_zero

Mathlib.CategoryTheory.ObjectProperty.Shift

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.shift_zero

← MathLib Explorer

English

Shifting by zero is the identity: P.shift 0 = P.

Русский

Сдвиг на ноль является тождественным преобразованием: P.shift 0 = P.

LaTeX

$$$P.shift(0) = P$$$

Lean4

@[simp]
theorem shift_zero [P.IsClosedUnderIsomorphisms] : P.shift (0 : A) = P :=
  by
  ext X
  exact P.prop_iff_of_iso ((shiftFunctorZero C A).app X)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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