Commit 2022-12-07 03:37 4bd624b2

View on Github →

feat: port Combinatorics.Quiver.Push (#868) mathlib3 SHA: 9b2660e1b25419042c8da10bf411aa3c67f14383

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Quiver/Push.lean

added theorem Push.lift_comp

added theorem Push.lift_obj

added theorem Push.lift_unique

added def Push.of

added theorem Push.of_obj

added def Push

added inductive PushQuiver