Commit 2022-12-01 17:40 a7641382

View on Github →

feat: port Combinatorics.Quiver.Path (#811) Mathlib3 SHA : 62a5626868683c104774de8d85b9855234ac807c

depends on: #749

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Quiver/Path.lean

added def Prefunctor.mapPath

added theorem Prefunctor.mapPath_comp

added theorem Prefunctor.mapPath_cons

added theorem Prefunctor.mapPath_nil

added theorem Prefunctor.mapPath_toPath

added def Quiver.Hom.toPath

added def Quiver.Path.comp

added theorem Quiver.Path.comp_assoc

added theorem Quiver.Path.comp_cons

added theorem Quiver.Path.comp_inj'

added theorem Quiver.Path.comp_inj

added theorem Quiver.Path.comp_inj_left

added theorem Quiver.Path.comp_inj_right

added theorem Quiver.Path.comp_injective_left

added theorem Quiver.Path.comp_injective_right

added theorem Quiver.Path.comp_nil

added theorem Quiver.Path.eq_of_length_zero

added def Quiver.Path.length

added theorem Quiver.Path.length_comp

added theorem Quiver.Path.length_cons

added theorem Quiver.Path.length_nil

added theorem Quiver.Path.nil_comp

added def Quiver.Path.toList

added theorem Quiver.Path.toList_chain_nonempty

added theorem Quiver.Path.toList_comp

added theorem Quiver.Path.toList_inj

added theorem Quiver.Path.toList_injective

added inductive Quiver.Path