Theorem CategoryTheory.Limits.inl_opProdIsoCoprod_inv

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.inl_opProdIsoCoprod_invView on Github →
2024-08-02 19:53
Mathlib/CategoryTheory/Limits/Opposites.lean
feat(AlgebraicGeometry/Limits): Spec preserves finite coproducts (#14428)
Added CategoryTheory.Limits.inl_opProdIsoCoprod_invView on Github →