Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-16 06:42 3db63953

View on Github →

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

Estimated changes

Modified src/category_theory/products/basic.lean

added def category_theory.functor.prod'_comp_fst

added def category_theory.functor.prod'_comp_snd

added def category_theory.functor_prod_functor_equiv

added def category_theory.functor_prod_functor_equiv_counit_iso

added def category_theory.functor_prod_functor_equiv_unit_iso

added def category_theory.functor_prod_to_prod_functor

added def category_theory.prod.eta_iso

added def category_theory.prod_functor_to_functor_prod