mathlib

c9ba7a5c - refactor(category_theory,algebra/category): make algebraic categories not [reducible] (#1491)

refactor(category_theory,algebra/category): make algebraic categories not [reducible] (#1491) * refactor(category_theory,algebra/category): make algebraic categories not [reducible] Adapted from part of #1438. * Update src/algebra/category/CommRing/basic.lean Co-Authored-By: Scott Morrison <scott@tqft.net> * adding missing forget2 instances * Converting Reid's comment to a [Note] * adding examples testing coercions