limits): fix typo, remove private
#1584

Merged

chore(algebra/category/CommRing/limits): fix typo, remove private #1584

mergify merged 9 commits into master from limits-cleanup

chore(algebra/category/CommRing/limits): fix typo, remove private

7ffac80a

Merge branch 'master' into limits-cleanup

aff7c053

jcommelin commented on 2019-10-22

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

d62824df

kim-em commented on 2019-10-22

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

36c0e886

kim-em commented on 2019-10-22

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

e9213080

bleh

97fd30e4

Merge branch 'master' into limits-cleanup

5816ee2f

kim-em commented on 2019-10-22

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

5d9d5aba

jcommelin added ready-to-merge

jcommelin approved these changes on 2019-10-22

Merge branch 'master' into limits-cleanup

3a227e76

mergify merged 31906d88 into master 6 years ago

mergify deleted the limits-cleanup branch 6 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone