Mathlib Map

Theorems · Definition · category theory

Quiver.SingleObj

Type u_1 → Type

Type tag on Unit used to define single-object quivers.

Defined in
Mathlib.Combinatorics.Quiver.SingleObj
Cited by
26 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.SingleObj · cited by 88CategoryTheory.SingleObjQuiver.SingleObj.star · cited by 17SingleObj.starQuiver.SingleObj.toPrefunctor · cited by 7SingleObj.toPrefunctorQuiver.SchreierGraph.labelling · cited by 6SchreierGraph.labellingQuiver.SchreierGraph.labellingCostarEquiv · cited by 4SchreierGraph.labellingCo…Quiver.SchreierGraph.labellingStarEquiv · cited by 4SchreierGraph.labellingSt…Quiver.SingleObj.pathEquivList · cited by 4SingleObj.pathEquivListQuiver.SingleObj.listToPath · cited by 3SingleObj.listToPathQuiver.SingleObj.pathToList · cited by 3SingleObj.pathToListQuiver.SingleObj.toHom · cited by 3SingleObj.toHomQuiver.SchreierGraph.labelling_map · cited by 1SchreierGraph.labelling_m…Quiver.SingleObj.ext · cited by 1SingleObj.extQuiver.SchreierGraph.labellingCostarEquiv_apply · cited by 0SchreierGraph.labellingCo…Quiver.SchreierGraph.labellingCostarEquiv_symm_apply_fst · cited by 0SchreierGraph.labellingCo…Quiver.SchreierGraph.labellingCostarEquiv_symm_apply_snd_coe · cited by 0SchreierGraph.labellingCo…Quiver.SingleObjCITED BYCITES

Cites0

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nothing in Mathlib beyond the foundations.

Cited by38

Results whose statement or proof uses this declaration.