mathlib
67e7f90d - fix(algebra/category): make has_coe_to_sort instances for bundled categories reducible (#2290)

Commit
5 years ago
fix(algebra/category): make has_coe_to_sort instances for bundled categories reducible (#2290) * fix(algebra/category): make has_coe_to_sort instances for bundled categories reducible * fix library notes * fix import * Update src/algebra/category/CommRing/basic.lean Co-Authored-By: Gabriel Ebner <gebner@gebner.org> * fix notes Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Gabriel Ebner <gebner@gebner.org> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Author
Parents
Loading