Theorem CategoryTheory.Functor.ofCoconeObjIso_hom_naturality

Modification history

2025-02-03 20:04
Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
refactor(CategoryTheory/SmallObject): generalization of the definitions (#20256) …
Deleted CategoryTheory.Functor.ofCoconeObjIso_hom_naturalityView on Github →
2024-12-21 09:50
Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
feat(CategoryTheory/SmallObject/Iteration): Functor.ofCocone (#19643) …
Added CategoryTheory.Functor.ofCoconeObjIso_hom_naturalityView on Github →