mathlib3
refactor(*): migrate some files to bundled ring homs
#2133

Merged

refactor(*): migrate some files to bundled ring homs #2133

mergify merged 8 commits into master from bundled-hom

refactor(*): migrate some files to bundled ring homs

2727e690

urkud requested a review from

jcommelin 6 years ago

Rename ring_hom.is_local back to is_local_ring_hom

e26c36f7

jcommelin commented on 2020-03-12

Apply suggestions from code review

c336f1da

Restore 2 instances, make `map` use bundled homs

947ef042

More bundled homs

c9e968b3

Merge branch 'bundled-hom' of git://github.com/leanprover-community/m…

de55130c

Merge branch 'master' into bundled-hom

f2237efa

urkud commented on 2020-03-13

Add a docstring

11ca5fed

urkud added awaiting-review

jcommelin commented on 2020-03-13

jcommelin removed awaiting-review

jcommelin approved these changes on 2020-03-13

jcommelin added ready-to-merge

mergify merged b54960d1 into master 6 years ago

mergify deleted the bundled-hom branch 6 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone