DinatTrans

📁 Source: Mathlib/CategoryTheory/DinatTrans.lean

Statistics

Metric	Count
Definitions DinatTrans, app, compNatTrans, precompNatTrans, «term_⤞_»	5
Theorems compNatTrans_app, dinaturality, dinaturality_assoc, precompNatTrans_app	4
Total	9

CategoryTheory

Definitions

Name	Category	Theorems
DinatTrans 📖	CompData	—

CategoryTheory.DinatTrans

Definitions

Name	Category	Theorems
app 📖	CompOp	4 math math: dinaturality_assoc, compNatTrans_app, precompNatTrans_app, dinaturality
compNatTrans 📖	CompOp	1 math math: compNatTrans_app
precompNatTrans 📖	CompOp	1 math math: precompNatTrans_app
«term_⤞_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compNatTrans_app 📖	mathematical	—	app compNatTrans CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.NatTrans.app	—	—
dinaturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver app	—	—
dinaturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver app	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' dinaturality
precompNatTrans_app 📖	mathematical	—	app precompNatTrans CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.NatTrans.app	—	—

---

← Back to Index