Def CategoryTheory.SmallObject.SuccStruct.ofCocone.objIsoPt

Modification history

2025-02-03 20:04

Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean

refactor(CategoryTheory/SmallObject): generalization of the definitions (#20256) …

Added CategoryTheory.SmallObject.SuccStruct.ofCocone.objIsoPt View on Github →