mathlib3
fix(algebra/category): make has_coe_to_sort instances for bundled categories reducible
#2290

Merged

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

mergify merged 7 commits into master from has_coe_to_sort_reducible

fix(algebra/category): make has_coe_to_sort instances for bundled cat…

a7344b98

kim-em requested a review from

rwbarton 5 years ago

kim-em requested a review from

urkud 5 years ago

kim-em requested a review from

gebner 5 years ago

fix library notes

07c9b955

gebner commented on 2020-03-30

fix import

435cea0a

Update src/algebra/category/CommRing/basic.lean

616b8726

fix notes

3a3bb9d4

Merge branch 'has_coe_to_sort_reducible' of github.com:leanprover-com…

b8f0e9ce

kim-em removed review request from

urkud 5 years ago

kim-em added awaiting-review

gebner approved these changes on 2020-03-31

gebner removed awaiting-review

gebner added ready-to-merge

Merge branch 'master' into has_coe_to_sort_reducible

b78bbb66

mergify merged 67e7f90d into master 5 years ago

robertylewis deleted the has_coe_to_sort_reducible branch 5 years ago

Reviewers

gebner

rwbarton

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone