Commit 2025-07-11 08:42 28819073

View on Github →

feat(CategoryTheory/Enriched): category of enriched functors (#26731)

Estimated changes

Modified Mathlib/CategoryTheory/Enriched/Basic.lean

added def CategoryTheory.EnrichedNatTrans.comp

added def CategoryTheory.EnrichedNatTrans.id

added theorem CategoryTheory.EnrichedNatTrans.naturality

Modified docs/references.bib