Def CategoryTheory.Functor.Iteration.restrictionLE

Modification history

2025-02-03 20:04
Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
refactor(CategoryTheory/SmallObject): generalization of the definitions (#20256) …
Deleted CategoryTheory.Functor.Iteration.restrictionLEView on Github →
2024-10-27 15:49
Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
feat(CategoryTheory/SmallObject): very basic API for the iteration of functors (#18115) …
Added CategoryTheory.Functor.Iteration.restrictionLEView on Github →