Theorem CategoryTheory.Limits.opProductIsoCoproduct'_comp_self

Modification history

2025-10-15 10:06

Mathlib/CategoryTheory/Limits/Opposites.lean

chore(CategoryTheory/Limits/Opposites): split the file Limits.Opposites (#30517) …

Modified CategoryTheory.Limits.opProductIsoCoproduct'_comp_self View on Github →

2024-04-17 10:18

Mathlib/CategoryTheory/Limits/Opposites.lean

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

Added CategoryTheory.Limits.opProductIsoCoproduct'_comp_self View on Github →