Commit 2025-02-01 21:35 388ed479

View on Github →

feat(CategoryTheory): creation of finite limits (#21320)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Limits/Creates.lean

added def CategoryTheory.createsColimitsOfShapeOfEquiv

added def CategoryTheory.createsLimitsOfShapeOfEquiv

Created Mathlib/CategoryTheory/Limits/Preserves/Creates/Finite.lean

added def CategoryTheory.Limits.CreatesColimitsOfSize.createsFiniteColimits

added def CategoryTheory.Limits.CreatesLimitsOfSize.createsFiniteLimits

added def CategoryTheory.Limits.createsFiniteColimitsOfCreatesFiniteColimitsOfSize

added def CategoryTheory.Limits.createsFiniteColimitsOfNatIso

added def CategoryTheory.Limits.createsFiniteCoproductsOfNatIso

added def CategoryTheory.Limits.createsFiniteLimitsOfCreatesFiniteLimitsOfSize

added def CategoryTheory.Limits.createsFiniteLimitsOfNatIso

added def CategoryTheory.Limits.createsFiniteProductsOfNatIso