Theorems · Definition · combinatorics
Quiver.Star
{U : Type u_1} → [Quiver U] → U → Type (max u_1 u)The Quiver.Star at a vertex is the collection of arrows whose source is the vertex.
The type Quiver.Star u is defined to be Σ (v : U), (u ⟶ v).
- Defined in
- Mathlib.Combinatorics.Quiver.Covering
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- Quiver
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homproof · cited by 32,603
- Quiverstatement and proof · cited by 405
Cited by30
Results whose statement or proof uses this declaration.
- Prefunctor.starstatement and proof · cited by 18
- Quiver.starEquivCostarstatement and proof · cited by 8
- Quiver.Star.mkstatement · cited by 7
- Prefunctor.IsCovering.star_bijectivestatement · cited by 6
- Quiver.SchreierGraph.labellingStarEquivstatement and proof · cited by 4
- Prefunctor.bijective_costar_iff_bijective_starstatement · cited by 2
- Quiver.symmetrifyCostarstatement · cited by 2
- Quiver.symmetrifyStarstatement · cited by 2
- Prefunctor.costar_conj_starstatement · cited by 1
- Prefunctor.pathStar_bijectivestatement · cited by 1
- Prefunctor.pathStar_injectivestatement · cited by 1
- Prefunctor.pathStar_surjectivestatement and proof · cited by 1