Commit 2023-08-12 18:26 cb48f57d

View on Github →

feat: port Combinatorics.Quiver.Covering (#6383)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Quiver/Covering.lean

added theorem Prefunctor.IsCovering.comp

added theorem Prefunctor.IsCovering.map_injective

added theorem Prefunctor.IsCovering.of_comp_left

added theorem Prefunctor.IsCovering.of_comp_right

added theorem Prefunctor.bijective_costar_iff_bijective_star

added def Prefunctor.costar

added theorem Prefunctor.costar_apply

added theorem Prefunctor.costar_comp

added theorem Prefunctor.costar_conj_star

added theorem Prefunctor.isCovering_of_bijective_costar

added theorem Prefunctor.isCovering_of_bijective_star

added def Prefunctor.pathStar

added theorem Prefunctor.pathStar_apply

added theorem Prefunctor.pathStar_bijective

added theorem Prefunctor.pathStar_injective

added theorem Prefunctor.pathStar_surjective

added def Prefunctor.star

added theorem Prefunctor.star_apply

added theorem Prefunctor.star_comp

added theorem Prefunctor.symmetrifyStar

added def Quiver.Costar

added def Quiver.PathStar

added def Quiver.Star

added def Quiver.starEquivCostar

added theorem Quiver.starEquivCostar_apply

added theorem Quiver.starEquivCostar_symm_apply

added def Quiver.symmetrifyCostar

added def Quiver.symmetrifyStar

Modified Mathlib/Combinatorics/Quiver/Symmetric.lean

added def Prefunctor.symmetrify