shiftFunctorComm_eq_refl

Mathlib.CategoryTheory.Shift.Basic

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

Lean4

@[simp]
theorem shiftFunctorComm_eq_refl (i : A) : shiftFunctorComm C i i = Iso.refl _ := by
  rw [shiftFunctorComm_eq C i i (i + i) rfl, Iso.symm_self_id]

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

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

Разделы

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

Аффилиация

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