limits): avoid `is_ring_hom`
#2142

Merged

chore(algebra/category/CommRing/limits): avoid `is_ring_hom` #2142

mergify merged 2 commits into master from commring-limits

chore(algebra/category/CommRing/limits): avoid `is_ring_hom`

7f7b94dc

jcommelin approved these changes on 2020-03-13

jcommelin added ready-to-merge

Merge branch 'master' into commring-limits

d36247b0

mergify merged 49f5fb88 into master 6 years ago

mergify deleted the commring-limits branch 6 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone