Theorem CategoryTheory.SmallObject.hasIterationOfShape

Modification history

2025-12-08 05:19

Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean

refactor: `Ordinal.toType` → `Ordinal.ToType` (#32449) …

Modified CategoryTheory.SmallObject.hasIterationOfShape View on Github →

2025-02-15 13:09

Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean

feat(CategoryTheory): cardinals that are suitable for the small object argument (#21865) …

Added CategoryTheory.SmallObject.hasIterationOfShape View on Github →