Commit 2021-03-20 16:28 5d7efa03

View on Github →

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 .

Estimated changes

Created src/combinatorics/quiver.lean

added theorem quiver.empty_arrow

added def quiver.labelling

added theorem quiver.opposite_arrow

added theorem quiver.opposite_opposite

added def quiver.path.length

added inductive quiver.path

added theorem quiver.sum_arrow

added def quiver.symmetrify

added theorem quiver.symmetrify_arrow

added def quiver.wide_subquiver_equiv_set_total

added def quiver.wide_subquiver_symmetrify

added structure quiver

added def wide_subquiver.quiver

added def wide_subquiver