Commit 2021-03-23 23:08 b6e4d0b9

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.