Mathlib Map

Theorems · Definition · combinatorics

Quiver.Hom

{V : Type u} → [self : Quiver V] → V → V → Type v

The type of edges/arrows/morphisms between a given source and target.

Defined in
Mathlib.Combinatorics.Quiver.Basic
Cited by
32,603 results in Mathlib
Foundations
Depth 1 from the axioms, rests on 2 definitions · uses no axioms
Assumes
Quiver
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CategoryTheory.CategoryStruct.comp · cited by 17999CategoryStruct.compCategoryTheory.Functor.map · cited by 8698Functor.mapCategoryTheory.Iso.hom · cited by 7684Iso.homCategoryTheory.NatTrans.app · cited by 7406NatTrans.appCategoryTheory.Functor.comp · cited by 6529Functor.compCategoryTheory.Iso.inv · cited by 6514Iso.invCategoryTheory.Category.assoc · cited by 6433Category.assocCategoryTheory.CategoryStruct.id · cited by 6235CategoryStruct.idCategoryTheory.ConcreteCategory.hom · cited by 4022ConcreteCategory.homCategoryTheory.Functor.id · cited by 3333Functor.idCategoryTheory.MorphismProperty · cited by 2179CategoryTheory.MorphismPr…CategoryTheory.Category.comp_id · cited by 2119Category.comp_idCategoryTheory.Category.id_comp · cited by 1998Category.id_compQuiver.Hom.op · cited by 1948Hom.opCategoryTheory.Functor.const · cited by 1264Functor.constQuiver · cited by 405QuiverQuiver.HomCITED BYCITES

Cites1

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

  • Quiverstatement and proof · cited by 405

Cited by43,134

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 43,134.