Commit 2025-03-13 11:07 4e3435ca

View on Github →

chore(CategoryTheory/Closed/Cartesian): make cartesian closed categories computable (#22896) Discussion on Zulip.

Estimated changes

Modified Mathlib/CategoryTheory/Closed/Cartesian.lean

deleted def CategoryTheory.cartesianClosedOfEquiv

modified def CategoryTheory.internalizeHom

modified def CategoryTheory.powZero

deleted def CategoryTheory.prodCoprodDistrib