Def CategoryTheory.Functor.extendToSucc

Modification history

2025-02-03 20:04
Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
refactor(CategoryTheory/SmallObject): generalization of the definitions (#20256) …
Deleted CategoryTheory.Functor.extendToSuccView on Github →
2024-11-30 09:05
Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
feat(CategoryTheory/SmallObject/Iteration): existence of objects (bot and succ cases) (#19047)
Added CategoryTheory.Functor.extendToSuccView on Github →