Theorem CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso_hom_naturality

Modification history

2025-02-03 20:04
Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
refactor(CategoryTheory/SmallObject): generalization of the definitions (#20256) …
Added CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso_hom_naturalityView on Github →