Structures · Combinatorics
Quiver.HasReverse
A quiver HasReverse if we can reverse an arrow p from a to b to get an arrow
p.reverse from b to a.
- Defined in
- Mathlib.Combinatorics.Quiver.Symmetric
- Shape
- One type argument · adds reverse'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances2
- Quiver.Symmetrify
- Quiver.Push
How is a type an instance?
Loading the hierarchy index…
Assumed by13
- Quiver.reverse
- Quiver.Path.reverse
- Quiver.Symmetrify.lift
- Quiver.Path.reverse_comp
- Quiver.Path.reverse_toPath
- Prefunctor.map_reverse
- Quiver.Symmetrify.lift_unique
- Quiver.Symmetrify.lift_spec
- Prefunctor.mapReverseComp
- Quiver.Path.reverse.eq_def
- Prefunctor.mapReverseId
- Quiver.Push.instHasReverse
- Quiver.HasReverse.reverse'
Ancestors0
No ancestors.