Commit 2024-10-10 08:57 09585751

View on Github →

chore(CategoryTheory/Limits/Shapes/BinaryProducts): Make some WalkingPair-related constructions computable (#17597) Change the computability of some constructions related to WalkingPair, so that mapPair, diagramIsoPair and pairComp are no longer marked as noncomputable.

Estimated changes

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

deleted def CategoryTheory.Limits.coprod.desc'

deleted def CategoryTheory.Limits.coprod.map

deleted def CategoryTheory.Limits.coprodIsCoprod

deleted def CategoryTheory.Limits.prod.lift'

deleted def CategoryTheory.Limits.prod.map

deleted def CategoryTheory.Limits.prodIsProd

deleted def CategoryTheory.Over.coprod

deleted def CategoryTheory.Over.coprodObj