Def CategoryTheory.Limits.colim.ι

Modification history

2026-09-07 10:31

Mathlib/CategoryTheory/Limits/HasLimits.lean

chore(CategoryTheory/Limits/HasLimits): use `to_dual` more (#42872) …

Deleted CategoryTheory.Limits.colim.ι View on Github →

2026-05-06 00:44

Mathlib/CategoryTheory/Limits/HasLimits.lean

refactor(CategoryTheory/Limits): redefine `IsIPC` in terms of `IsIPCOfShape` (#38378) …

Added CategoryTheory.Limits.colim.ι View on Github →