Theorem CategoryTheory.Functor.Iteration.Hom.mkOfSuccNatTransApp_eq_of_le

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.mkOfSuccNatTransApp_eq_of_leView 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.mkOfSuccNatTransApp_eq_of_leView on Github →