Structures · Combinatorics
Quiver.HasInvolutiveReverse
A quiver HasInvolutiveReverse if reversing twice is the identity.
- Defined in
- Mathlib.Combinatorics.Quiver.Symmetric
- Shape
- One type argument · adds inv'
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Quiver.Symmetrify
- Quiver.Push
How is a type an instance?
Loading the hierarchy index…
Assumed by21
- Quiver.starEquivCostar
- Quiver.reverse_reverse
- Prefunctor.bijective_costar_iff_bijective_star
- Quiver.reverse_inj
- Quiver.Path.reverse_reverse
- Prefunctor.costar_conj_star
- Quiver.HasInvolutiveReverse.inv'
- Quiver.starEquivCostar_apply
- Quiver.Push.instHasInvolutiveReverse
- Quiver.starEquivCostar_apply_snd
- Quiver.starEquivCostar_symm_apply_snd
- Quiver.Push.of_reverse
- Quiver.HasInvolutiveReverse.toHasReverse
- Quiver.starEquivCostar_apply_fst
- Prefunctor.isCovering_of_bijective_costar
- Prefunctor.isCovering_of_bijective_star
- Quiver.Push.ofMapReverse
- Quiver.starEquivCostar_symm_apply
- Quiver.starEquivCostar_symm_apply_fst
- Quiver.eq_reverse_iff
- Quiver.Symmetrify.lift_reverse