Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-20 07:56 944ffff9

View on Github →

chore(combinatorics/quiver): make quiver a class (#7150)

Estimated changes

Modified src/combinatorics/quiver.lean

deleted def quiver.arrow.reverse

deleted def quiver.arrow.to_path

added def quiver.empty

modified theorem quiver.empty_arrow

modified def quiver.geodesic_subtree

added def quiver.hom.to_path

modified def quiver.labelling

deleted theorem quiver.opposite_arrow

deleted theorem quiver.opposite_opposite

modified def quiver.path.comp

modified theorem quiver.path.comp_assoc

modified theorem quiver.path.comp_cons

modified theorem quiver.path.comp_nil

modified def quiver.path.length

modified theorem quiver.path.length_cons

modified theorem quiver.path.nil_comp

modified def quiver.path.reverse

modified inductive quiver.path

added def quiver.reverse

added def quiver.root

modified theorem quiver.shortest_path_spec

deleted theorem quiver.sum_arrow

modified def quiver.symmetrify

deleted theorem quiver.symmetrify_arrow

added structure quiver.total

modified def quiver.weakly_connected_component

modified def quiver.wide_subquiver_equiv_set_total

modified def quiver.wide_subquiver_symmetrify

deleted structure quiver

deleted def wide_subquiver.quiver

added def wide_subquiver.to_Type

modified def wide_subquiver