Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-03 15:52 7ba713a7

View on Github →

feat(quiver/basic): push arrows of a quiver along a map (#17618)

Estimated changes

added def push.lift
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 push_quiver