Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-03-11 14:23
07ab9d6a
View on Github →
feat: port CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (
#2764
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean
added
def
CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit
added
def
CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildIsColimit
added
def
CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildIsLimit
added
def
CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit
added
theorem
CategoryTheory.Limits.hasColimit_of_coequalizer_and_coproduct
added
theorem
CategoryTheory.Limits.hasFiniteColimits_of_hasCoequalizers_and_finite_coproducts
added
theorem
CategoryTheory.Limits.hasFiniteColimits_of_hasInitial_and_pushouts
added
theorem
CategoryTheory.Limits.hasFiniteLimits_of_hasEqualizers_and_finite_products
added
theorem
CategoryTheory.Limits.hasFiniteLimits_of_hasTerminal_and_pullbacks
added
theorem
CategoryTheory.Limits.hasLimit_of_equalizer_and_product
added
theorem
CategoryTheory.Limits.has_colimits_of_hasCoequalizers_and_coproducts
added
theorem
CategoryTheory.Limits.has_limits_of_hasEqualizers_and_products
Modified
Mathlib/CategoryTheory/Limits/Preserves/Finite.lean