Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-11-28 16:12
2f728e97
View on Github →
chore: split Prefunctor out of Quiver (
#19525
)
Estimated changes
Modified
Mathlib.lean
Modified
Mathlib/CategoryTheory/Functor/Basic.lean
Modified
Mathlib/Combinatorics/Quiver/Basic.lean
deleted
def
Prefunctor.comp
deleted
theorem
Prefunctor.comp_assoc
deleted
theorem
Prefunctor.comp_id
deleted
theorem
Prefunctor.congr_map
deleted
theorem
Prefunctor.ext
deleted
def
Prefunctor.id
deleted
theorem
Prefunctor.id_comp
deleted
theorem
Prefunctor.mk_map
deleted
theorem
Prefunctor.mk_obj
deleted
structure
Prefunctor
Modified
Mathlib/Combinatorics/Quiver/Path.lean
Created
Mathlib/Combinatorics/Quiver/Prefunctor.lean
added
def
Prefunctor.comp
added
theorem
Prefunctor.comp_assoc
added
theorem
Prefunctor.comp_id
added
theorem
Prefunctor.congr_map
added
theorem
Prefunctor.ext
added
def
Prefunctor.id
added
theorem
Prefunctor.id_comp
added
theorem
Prefunctor.mk_map
added
theorem
Prefunctor.mk_obj
added
structure
Prefunctor
Modified
Mathlib/Combinatorics/Quiver/Push.lean