Theorem CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_left

Modification history

2025-12-08 05:19
Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
refactor: `Ordinal.toType` → `Ordinal.ToType` (#32449) …
Modified CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_leftView on Github →
2025-02-15 18:13
Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
feat(CategoryTheory/SmallObject): the functorial factorization (#21911) …
Added CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_leftView on Github →