-
Notifications
You must be signed in to change notification settings - Fork 299
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(data/mv_polynomial): define comap #4161
Conversation
no idea where 2017 came from
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would have expected to see a lemma along the lines of comap (rename f) x = x \circ f
, but apparently rename
should first be made an alg_hom
. If you don't want to redefine rename
, I'm happy with merging as is (after removing a few unnecessary brackets).
bors d+
✌️ robertylewis can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
@Vierkantor done |
Thanks! bors r+ |
More from the Witt vector branch. Co-authored by: Johan Commelin <johan@commelin.net> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>
Pull request successfully merged into master. Build succeeded: |
More from the Witt vector branch.
Co-authored by: Johan Commelin johan@commelin.net