Def category_theory.prod_functor_to_functor_prod

Modification history

2022-08-16 06:42

src/category_theory/products/basic.lean

feat(category_theory/products/basic): equivalence ((A ⥤ B) × (A ⥤ C)) ≌ (A ⥤ (B × C)) (#15445)

Added category_theory.prod_functor_to_functor_prod View on Github →