mathlib
f474756b - chore(category_theory/abelian): enable instances (#7106)

Commit
4 years ago
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. Co-authored-by: Markus Himmel <markus@himmel-villmar.de> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading