Commit 2024-04-17 10:18 423f5783

View on Github →

feat(CategoryTheory): a lemma about composing different isomorphisms from opposite coproducts to products (#12155)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Opposites.lean

added theorem CategoryTheory.Limits.opCoproductIsoProduct'_comp_self

added theorem CategoryTheory.Limits.opProductIsoCoproduct'_comp_self

deleted theorem CategoryTheory.Limits.proj_comp_opProductIsoCoproduct_hom

added theorem CategoryTheory.Limits.π_comp_opProductIsoCoproduct_hom