Commit 2021-04-01 09:03 a9b6230a

View on Github →

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.

Estimated changes

Modified src/combinatorics/quiver.lean

added def quiver.arrow.reverse

added def quiver.arrow.to_path

added def quiver.path.comp

added theorem quiver.path.comp_assoc

added theorem quiver.path.comp_cons

added theorem quiver.path.comp_nil

modified def quiver.path.length

modified theorem quiver.path.length_cons

modified theorem quiver.path.length_nil

added theorem quiver.path.nil_comp

added def quiver.path.reverse

added def quiver.weakly_connected_component

added def quiver.zigzag_setoid