Commit 2022-12-17 08:37 32618bfa

View on Github →

feat: Refactor ConnectedComponent (#971) … in order to sync with PR 17665 on mathlib3. See https://github.com/leanprover-community/mathlib/pull/17665

Estimated changes

deleted def Quiver.Path.reverse
deleted theorem Quiver.Path.reverse_comp
deleted def Quiver.Symmetrify
deleted def Quiver.reverse
deleted theorem Quiver.reverse_reverse
deleted theorem Push.lift_comp
deleted theorem Push.lift_obj
deleted theorem Push.lift_unique
deleted def Push.of
deleted theorem Push.of_obj
deleted def Push
deleted inductive PushQuiver
added theorem Quiver.Push.lift_comp
added theorem Quiver.Push.lift_obj
added def Quiver.Push.of
added theorem Quiver.Push.of_obj
added def Quiver.Push
added inductive Quiver.PushQuiver
added theorem Prefunctor.map_reverse
added theorem Quiver.Push.of_reverse
added theorem Quiver.eq_reverse_iff
added def Quiver.reverse
added theorem Quiver.reverse_inj
added theorem Quiver.reverse_reverse