Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(algebra/*/ulift): algebraic instances for ulift #3675

Closed
wants to merge 11 commits into from
Closed

[Merged by Bors] - feat(algebra/*/ulift): algebraic instances for ulift #3675

wants to merge 11 commits into from

Conversation

semorrison
Copy link
Collaborator

@semorrison semorrison mentioned this pull request Aug 3, 2020
Closed
@TwoFX
Copy link
Member

TwoFX commented Aug 3, 2020

With a view to the discussion at #3621, it might be useful to add instance(s) for (semi)module.

@semorrison
Copy link
Collaborator Author

Yes --- but where should I put the ulift? On the scalar or on the module, or both? I got a bit confused on this issue and decided to stop. :-)

@TwoFX
Copy link
Member

TwoFX commented Aug 3, 2020

I think what we need for #3621 is ulift on the scalar, but I guess having the other two options for completeness won't hurt.

@semorrison
Copy link
Collaborator Author

Okay, I think I did both ways.

@Vierkantor
Copy link
Collaborator

I only see a change in src/algebra/module/pi.lean, did you forget to add your new file?

@PatrickMassot PatrickMassot added the awaiting-author A reviewer has asked the author a question or requested changes label Aug 3, 2020
@semorrison semorrison added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Aug 3, 2020
@semorrison
Copy link
Collaborator Author

@Vierkantor, oops, sorry. I've added the new file now.

TwoFX
TwoFX reviewed Aug 4, 2020
View reviewed changes
src/algebra/module/ulift.lean Outdated Show resolved Hide resolved
src/algebra/ring/ulift.lean Outdated Show resolved Hide resolved
Vierkantor
Vierkantor approved these changes Aug 4, 2020
View reviewed changes
Copy link
Collaborator

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM.

@robertylewis
Copy link
Member

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Aug 5, 2020
bors bot pushed a commit that referenced this pull request Aug 5, 2020
@semorrison
feat(algebra/*/ulift): algebraic instances for ulift (#3675)
4a82e84 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Aug 5, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra/*/ulift): algebraic instances for ulift [Merged by Bors] - feat(algebra/*/ulift): algebraic instances for ulift Aug 5, 2020
@bors bors bot closed this Aug 5, 2020
@bors bors bot deleted the ulift_instances branch August 5, 2020 12:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@TwoFX TwoFX TwoFX left review comments

@bryangingechen bryangingechen bryangingechen left review comments

@Vierkantor Vierkantor Vierkantor approved these changes

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@semorrison @TwoFX @Vierkantor @robertylewis @bryangingechen @PatrickMassot