mathlib3

b6e4d0b9 - feat(combinatorics/quiver): every connected graph has a spanning tree (#6806)

feat(combinatorics/quiver): every connected graph has a spanning tree (#6806) Prove a directed version of the fact that a connected graph has a spanning tree. The subtree we use is what you would get from 'running a DFS from the root'. This proof avoids any use of Zorn's lemma. Currently we have no notion of undirected tree, but once that is in place, this proof should also give undirected spanning trees.