Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-02-02 12:28
7eeba0a7
View on Github →
feat: creation of products and equalizers implies creation of limits (
#21321
)
Estimated changes
Modified
Mathlib/Algebra/Category/Grp/Ulift.lean
Modified
Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean
Modified
Mathlib/CategoryTheory/Limits/Creates.lean
deleted
def
CategoryTheory.createsColimitOfFullyFaithfulOfPreserves
added
def
CategoryTheory.createsColimitOfReflectsIsomorphismsOfPreserves
added
def
CategoryTheory.createsLimitOfReflectsIsomorphismsOfPreserves
Modified
Mathlib/CategoryTheory/Limits/Preserves/Finite.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Ulift.lean