Theorems · Definition · category theory
CategoryTheory.MonoidalCategoryStruct.tensorUnit
(C : Type u) → {𝒞 : CategoryTheory.Category.{v, u} C} → [self : CategoryTheory.MonoidalCategoryStruct C] → CThe tensor unity in the monoidal structure 𝟙_ C
- Defined in
- Mathlib.CategoryTheory.Monoidal.Category
- Cited by
- 1,384 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 by1,727
Results whose statement or proof uses this declaration.
- CategoryTheory.MonoidalCategoryStruct.leftUnitorstatement · cited by 437
- CategoryTheory.MonoidalCategoryStruct.rightUnitorstatement · cited by 397
- CategoryTheory.Functor.LaxMonoidal.εstatement · cited by 202
- CategoryTheory.MonObj.onestatement · cited by 189
- CategoryTheory.Functor.OplaxMonoidal.ηstatement · cited by 159
- CategoryTheory.SemiCartesianMonoidalCategory.toUnitstatement · cited by 103
- CategoryTheory.AddMonObj.zerostatement · cited by 100
- CategoryTheory.ComonObj.counitstatement · cited by 67
- CategoryTheory.LocalizedMonoidalstatement and proof · cited by 55
- CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIsostatement · cited by 39
- CategoryTheory.MonoidalCategory.whiskerRight_idstatement and proof · cited by 38
- CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIsostatement · cited by 32
Showing the 200 most cited of 1,727.