Theorems · Theorem · category theory
CategoryTheory.Category.assoc
∀ {obj : Type u} [self : CategoryTheory.Category.{v, u} obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h =
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)Composition in a category is associative.
- Defined in
- Mathlib.CategoryTheory.Category.Basic
- Cited by
- 6,433 results in Mathlib
- Foundations
- Depth 3 from the axioms, rests on 8 definitions · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homstatement · cited by 32,603
- CategoryTheory.CategoryStruct.compstatement · cited by 17,999
Cited by6,442
Results whose statement or proof uses this declaration.
- CategoryTheory.Iso.inv_hom_id_assocproof · cited by 275
- CategoryTheory.Iso.hom_inv_id_assocproof · cited by 187
- CategoryTheory.Limits.limit.lift_π_assocproof · cited by 95
- CategoryTheory.NatTrans.naturality_assocproof · cited by 68
- CategoryTheory.Iso.inv_hom_id_app_assocproof · cited by 57
- CategoryTheory.Limits.prod.comp_liftproof · cited by 46
- CategoryTheory.Limits.colimit.ι_desc_assocproof · cited by 44
- CategoryTheory.Iso.comp_inv_eqproof · cited by 41
- CategoryTheory.Iso.hom_inv_id_app_assocproof · cited by 40
- CategoryTheory.Iso.trans_assocproof · cited by 39
- CategoryTheory.MonoidalCategory.whiskerRight_idproof · cited by 38
- CategoryTheory.IsIso.inv_hom_id_assocproof · cited by 37
Showing the 200 most cited of 6,442.