feat(combinatorics/quiver): define quivers (#6680)
feat(combinatorics/quiver): define quivers (#6680)

Define quivers (a very permissive notion of graph), subquivers, paths
and arborescences, which are like rooted trees.

This PR comes from https://github.com/dwarn/nielsen-schreier-2 .







leanprover-community/mathlib,leanprover-community/mathlib