mathlib3
chore(algebra/ring): change semiring_hom to ring_hom
#1361
Merged
Overview
Commits
12
Changes
View On GitHub

chore(algebra/ring): change semiring_hom to ring_hom #1361

mergify merged 12 commits into master from bundled_ring_homs
101damnations
added bundled ring homs
eec41e69
removed comment
77143069
Tidy and making docstrings consistent
45281824
jcommelin fix spacing
0797bb14
101damnations fix typo
c02a30d5
101damnations fix typo
5477a1d2
Removing instances and editing docstrings
28c6bb83
whoops, actually removing instances
9c84a331
101damnations update mathlib
d186e4d8
101damnations change semiring_hom to ring_hom
514c0c78
101damnations corrected docstring
37a847ba
101damnations 101damnations requested a review 6 years ago
101damnations Merge branch 'master' into bundled_ring_homs
3e506b05
jcommelin
jcommelin commented on 2019-08-26
ChrisHughes24
ChrisHughes24 approved these changes on 2019-08-26
ChrisHughes24 ChrisHughes24 added ready-to-merge
mergify mergify merged cc04ba7e into master 6 years ago
mergify mergify deleted the bundled_ring_homs branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum