Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-18 11:08 56adee5b

View on Github →

feat(combinatorics/quiver/single_obj): single object quivers (#17846) I think it makes sense for category_theory/single_obj to depend on combinatorics/quiver/single_obj, but I'd like to know what people working with category theory think of that. Co-authored by: Remi Bottinelli https://github.com/bottine

Estimated changes

Modified src/category_theory/single_obj.lean

added def category_theory.single_obj.star

modified def category_theory.single_obj

Modified src/combinatorics/quiver/basic.lean

Created src/combinatorics/quiver/single_obj.lean

added def quiver.single_obj.has_involutive_reverse

added def quiver.single_obj.has_reverse

added def quiver.single_obj.list_to_path

added theorem quiver.single_obj.list_to_path_to_list

added def quiver.single_obj.path_equiv_list

added theorem quiver.single_obj.path_equiv_list_cons

added theorem quiver.single_obj.path_equiv_list_nil

added theorem quiver.single_obj.path_equiv_list_symm_cons

added theorem quiver.single_obj.path_equiv_list_symm_nil

added def quiver.single_obj.path_to_list

added theorem quiver.single_obj.path_to_list_to_path

added def quiver.single_obj.star

added def quiver.single_obj.to_hom

added def quiver.single_obj.to_prefunctor

added theorem quiver.single_obj.to_prefunctor_comp

added theorem quiver.single_obj.to_prefunctor_id

added theorem quiver.single_obj.to_prefunctor_symm_comp

added theorem quiver.single_obj.to_prefunctor_symm_id

added def quiver.single_obj

Modified src/group_theory/nielsen_schreier.lean