Commit 2023-06-27 08:51 a5af4e3c

View on Github →

feat: port CategoryTheory.Closed.Ideal (#4951)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Closed/Ideal.lean

added theorem CategoryTheory.ExponentialIdeal.mk'

added theorem CategoryTheory.ExponentialIdeal.mk_of_iso

added theorem CategoryTheory.bijection_natural

added theorem CategoryTheory.bijection_symm_apply_id

added def CategoryTheory.cartesianClosedOfReflective

added def CategoryTheory.exponentialIdealReflective

added theorem CategoryTheory.prodComparison_iso

added theorem CategoryTheory.reflective_products