Commit 2023-07-31 16:57 2c4229d9

View on Github →

feat: iterated categorical (co/bi/)products (#6255)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

added theorem CategoryTheory.Limits.Bicone.toCocone_proj

added theorem CategoryTheory.Limits.Bicone.toCone_proj

added def CategoryTheory.Limits.biproductBiproductIso

Modified Mathlib/CategoryTheory/Limits/Shapes/Products.lean

modified def CategoryTheory.Limits.Cofan.mk

added def CategoryTheory.Limits.Cofan.proj

modified def CategoryTheory.Limits.Fan.mk

added theorem CategoryTheory.Limits.cofan_mk_proj

added def CategoryTheory.Limits.mkCofanColimit

added def CategoryTheory.Limits.piPiIso

added def CategoryTheory.Limits.sigmaSigmaIso