Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-24 01:00 bfc8c66b

View on Github →

feat(category_theory/limits/shapes/finite*): finite limits from limits (#3800) Add some missing derivations in the new has_limits hierarchy

Estimated changes

Modified src/category_theory/limits/shapes/finite_limits.lean

added def category_theory.limits.has_finite_colimits_of_has_colimits

added def category_theory.limits.has_finite_limits_of_has_limits

Modified src/category_theory/limits/shapes/finite_products.lean

added def category_theory.limits.has_finite_coproducts_of_has_finite_colimits

added def category_theory.limits.has_finite_products_of_has_finite_limits