Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-08 14:49 f474756b

View on Github →

chore(category_theory/abelian): enable instances (#7106) This PR is extracted from Markus' projective branch. It just turns on, as global instances, various instances provided by an abelian category. In the past these weren't instances, because has_limit carried data which could conflict.

Estimated changes