Commit 2024-09-25 14:12 a95aae11

View on Github →

feat(CategoryTheory/Limits): dualize Pi.isoLimit to Sigma.isoColimit (#17076)

Estimated changes

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

added def CategoryTheory.Limits.Sigma.cocone

added def CategoryTheory.Limits.Sigma.isoColimit

added theorem CategoryTheory.Limits.Sigma.ι_isoColimit_hom

added theorem CategoryTheory.Limits.Sigma.ι_isoColimit_inv

added def CategoryTheory.Limits.coproductIsCoproduct'