Theorem CategoryTheory.Limits.Pi.map_eq_prod_map

Modification history

2024-12-20 05:45
Mathlib/CategoryTheory/Limits/Shapes/PiProd.lean
chore(*): drop some `[Decidable*]` assumptions (#19988) …
Modified CategoryTheory.Limits.Pi.map_eq_prod_mapView on Github →
2024-11-26 12:47
Mathlib/CategoryTheory/Limits/Shapes/PiProd.lean
feat(CategoryTheory): split up a product into a binary product (#19199)
Added CategoryTheory.Limits.Pi.map_eq_prod_mapView on Github →