Def category_theory.prod.eta_iso

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.eta_iso View on Github →