Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-10 08:44 ac669c74

View on Github →

chore(category_theory/limits/preserves): cleanup (#4163) (edited to update). This PR entirely re-does the construction of limits from products and equalizers in a shorter way. With the new preserves limits machinery this new construction also shows that a functor which preserves products and equalizers preserves all limits, which previously was really annoying to do

Estimated changes