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