Commit 2022-12-04 12:55 e710a7be

View on Github →

feat: port Combinatorics.Quiver.ConnectedComponent (#836)

feat: port Combinatorics.Quiver.ConnectedComponent
pleased lint

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Quiver/ConnectedComponent.lean

added def Quiver.Path.reverse

added theorem Quiver.Path.reverse_comp

added theorem Quiver.Path.reverse_reverse

added theorem Quiver.Path.reverse_toPath

added def Quiver.Symmetrify.lift

added theorem Quiver.Symmetrify.lift_reverse

added theorem Quiver.Symmetrify.lift_spec

added theorem Quiver.Symmetrify.lift_unique

added def Quiver.Symmetrify.of

added def Quiver.Symmetrify

added def Quiver.WeaklyConnectedComponent

added def Quiver.reverse

added theorem Quiver.reverse_reverse

added def Quiver.wideSubquiverSymmetrify

added def Quiver.zigzagSetoid