Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-08 16:28 b181a120

View on Github →

refactor(combinatorics/quiver): split into several files (#11006) This PR splits combinatorics/quiver.lean into several files. The main reason for this is to ensure that the category theory library only imports the necessary definitions (and not for example the stuff on arborescences). Also adds some more documentation, and fixes a bug in the definition of weakly connected components.

Estimated changes

deleted def prefunctor.comp
deleted def prefunctor.id
deleted def prefunctor.map_path
deleted theorem prefunctor.map_path_comp
deleted theorem prefunctor.map_path_cons
deleted theorem prefunctor.map_path_nil
deleted structure prefunctor
deleted def quiver.empty
deleted theorem quiver.empty_arrow
deleted def quiver.hom.op
deleted def quiver.hom.to_path
deleted def quiver.hom.unop
deleted def quiver.labelling
deleted def quiver.path.comp
deleted theorem quiver.path.comp_assoc
deleted theorem quiver.path.comp_cons
deleted theorem quiver.path.comp_nil
deleted def quiver.path.length
deleted theorem quiver.path.length_cons
deleted theorem quiver.path.length_nil
deleted theorem quiver.path.nil_comp
deleted def quiver.path.reverse
deleted inductive quiver.path
deleted def quiver.reverse
deleted def quiver.root
deleted theorem quiver.shortest_path_spec
deleted def quiver.symmetrify
deleted structure quiver.total
deleted def wide_subquiver
added def quiver.root
added def prefunctor.comp
added def prefunctor.id
added structure prefunctor
added def quiver.empty
added theorem quiver.empty_arrow
added def quiver.hom.op
added def quiver.hom.unop
added def quiver.reverse
added def quiver.path.comp
added theorem quiver.path.comp_assoc
added theorem quiver.path.comp_cons
added theorem quiver.path.comp_nil
added theorem quiver.path.length_nil
added theorem quiver.path.nil_comp
added inductive quiver.path
added def quiver.labelling
added structure quiver.total
added def wide_subquiver