Def CategoryTheory.Functor.Iteration.Hom.mkOfBot

Modification history

2025-02-03 20:04

Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean

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

Deleted CategoryTheory.Functor.Iteration.Hom.mkOfBot View on Github →

2024-11-10 22:20

Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean

feat(CategoryTheory/SmallObject/Iteration): the unique morphism (bot and succ cases) (#18127)

Added CategoryTheory.Functor.Iteration.Hom.mkOfBot View on Github →