Commit 2023-01-20 21:53 e292ba03

View on Github →

feat: port combinatorics.quiver.single obj (#1686)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Quiver/SingleObj.lean

added theorem Quiver.SingleObj.ext

added def Quiver.SingleObj.hasInvolutiveReverse

added def Quiver.SingleObj.hasReverse

added def Quiver.SingleObj.listToPath

added theorem Quiver.SingleObj.listToPath_pathToList

added def Quiver.SingleObj.pathEquivList

added theorem Quiver.SingleObj.pathEquivList_cons

added theorem Quiver.SingleObj.pathEquivList_nil

added theorem Quiver.SingleObj.pathEquivList_symm_cons

added theorem Quiver.SingleObj.pathEquivList_symm_nil

added def Quiver.SingleObj.pathToList

added theorem Quiver.SingleObj.pathToList_listToPath

added def Quiver.SingleObj.star

added def Quiver.SingleObj.toHom

added def Quiver.SingleObj.toPrefunctor

added theorem Quiver.SingleObj.toPrefunctor_comp

added theorem Quiver.SingleObj.toPrefunctor_id

added theorem Quiver.SingleObj.toPrefunctor_symm_comp

added theorem Quiver.SingleObj.toPrefunctor_symm_id

added def Quiver.SingleObj