Theorems · Definition · category theory
CategoryTheory.Quiv
Type (max (u + 1) u (v + 1))
Category of quivers.
- Defined in
- Mathlib.CategoryTheory.Category.Quiv
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
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.
- Quiverproof · cited by 405
- CategoryTheory.Bundledproof · cited by 42
Cited by34
Results whose statement or proof uses this declaration.
- CategoryTheory.Quiv.ofstatement · cited by 8
- CategoryTheory.Quiv.forgetstatement · cited by 5
- CategoryTheory.ReflQuiv.forgetToQuivstatement · cited by 4
- CategoryTheory.Cat.freestatement and proof · cited by 4
- CategoryTheory.Quiv.equivOfIsostatement and proof · cited by 4
- CategoryTheory.Prefunctor.ofQuivHomstatement and proof · cited by 3
- CategoryTheory.Prefunctor.toQuivHomstatement · cited by 2
- CategoryTheory.Quiv.adjstatement and proof · cited by 2
- CategoryTheory.Quiv.homEquivOfIsostatement and proof · cited by 2
- CategoryTheory.Quiv.hom_map_inv_map_of_isostatement and proof · cited by 1
- CategoryTheory.Quiv.homEquivOfIso_symm_applystatement and proof · cited by 0
- CategoryTheory.Quiv.hom_obj_inv_obj_of_isostatement and proof · cited by 0