Commit 2024-11-26 12:47 5d0ac044

View on Github →

feat(CategoryTheory): split up a product into a binary product (#19199)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Shapes/PiProd.lean

added theorem CategoryTheory.Limits.Pi.map_eq_prod_map

added theorem CategoryTheory.Limits.hasBinaryProduct_of_products