Theorems · Definition · category theory
CategoryTheory.MonoidalCategoryStruct.tensorObj
{C : Type u} → {𝒞 : CategoryTheory.Category.{v, u} C} → [self : CategoryTheory.MonoidalCategoryStruct C] → C → C → Ccurried tensor product of objects
- Defined in
- Mathlib.CategoryTheory.Monoidal.Category
- Cited by
- 3,106 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 3 definitions · 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.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.MonoidalCategoryStructstatement and proof · cited by 26
Cited by3,585
Results whose statement or proof uses this declaration.
- CategoryTheory.MonoidalCategoryStruct.whiskerLeftstatement · cited by 915
- CategoryTheory.MonoidalCategoryStruct.whiskerRightstatement · cited by 903
- CategoryTheory.MonoidalCategoryStruct.associatorstatement · cited by 667
- CategoryTheory.MonoidalCategoryStruct.tensorHomstatement · cited by 587
- CategoryTheory.MonoidalCategoryStruct.leftUnitorstatement · cited by 437
- CategoryTheory.MonoidalCategoryStruct.rightUnitorstatement · cited by 397
- CategoryTheory.Functor.LaxMonoidal.μstatement · cited by 285
- CategoryTheory.BraidedCategory.braidingstatement · cited by 257
- CategoryTheory.MonObj.mulstatement · cited by 230
- CategoryTheory.Functor.OplaxMonoidal.δstatement · cited by 222
- CategoryTheory.SemiCartesianMonoidalCategory.fststatement · cited by 184
- CategoryTheory.SemiCartesianMonoidalCategory.sndstatement · cited by 181
Showing the 200 most cited of 3,585.