mathlib3

a9b6230a - feat(combinatorics/quiver): weakly connected components (#6847)

feat(combinatorics/quiver): weakly connected components (#6847) Define composition of paths and the weakly connected components of a directed graph. Two vertices are in the same weakly connected component if there is a zigzag of arrows from one to the other.