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/char_p): characteristic of fraction_ring #7703

Closed
wants to merge 19 commits into from
Closed

[Merged by Bors] - feat(algebra/char_p): characteristic of fraction_ring #7703

wants to merge 19 commits into from

Conversation

joneugster
Copy link
Collaborator

Adding the characteristics of a fraction_ring for an integral domain.

Open in Gitpod

@joneugster joneugster added help-wanted The author needs attention to resolve issues awaiting-review The author would like community review of the PR labels May 24, 2021
@joneugster @eric-wieser
Update src/algebra/char_p/localization.lean
22e8488 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@joneugster joneugster changed the title Char p localization feat(algebra/char_p): characteristic of fraction_ring May 24, 2021
ericrbg
ericrbg reviewed May 24, 2021
View reviewed changes
src/algebra/char_p/localization.lean Outdated Show resolved Hide resolved
src/algebra/char_p/localization.lean Outdated Show resolved Hide resolved
src/algebra/char_p/localization.lean Outdated Show resolved Hide resolved
src/algebra/char_p/localization.lean Outdated Show resolved Hide resolved
joneugster and others added 3 commits May 24, 2021 15:55
@joneugster @ericrbg
Update src/algebra/char_p/localization.lean
08d85bb 
Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>
@joneugster @ericrbg
Update src/algebra/char_p/localization.lean
7152d40 
Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>
@joneugster @ericrbg
Update src/algebra/char_p/localization.lean
5134c5d 
Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>
@joneugster joneugster added WIP Work in progress and removed awaiting-review The author would like community review of the PR help-wanted The author needs attention to resolve issues labels May 24, 2021
@joneugster joneugster added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels May 24, 2021
eric-wieser
eric-wieser reviewed May 26, 2021
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

I think it might make sense to use this to also provide char_zero and char_p instances on free_algebra given we have a proof of free_algebra.algebra_map_left_inverse.injective.

Are you ok to do that, or would you prefer to declare it out of scope?

src/algebra/char_p/algebra.lean Outdated Show resolved Hide resolved
src/algebra/char_p/algebra.lean Outdated Show resolved Hide resolved
@joneugster
Copy link
Collaborator Author

bors r+

@joneugster
Copy link
Collaborator Author

bors cancel

@bors
Copy link

bors bot commented Jun 1, 2021

Canceled.

@joneugster joneugster added awaiting-review The author would like community review of the PR and removed delegated The PR author may merge after reviewing final suggestions. labels Jun 1, 2021
@semorrison semorrison added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jun 2, 2021
@joneugster joneugster 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 Jun 2, 2021
joneugster and others added 2 commits June 2, 2021 12:41
@joneugster @eric-wieser
docstring
a2a02f0 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@joneugster
docstring typo
bfea25d
@semorrison
Copy link
Collaborator

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 Jun 6, 2021
bors bot pushed a commit that referenced this pull request Jun 6, 2021
@joneugster @eric-wieser
feat(algebra/char_p): characteristic of fraction_ring (#7703)
e3f897c 
Adding the characteristics of a `fraction_ring` for an integral domain.



Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@bors
Copy link

bors bot commented Jun 6, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra/char_p): characteristic of fraction_ring [Merged by Bors] - feat(algebra/char_p): characteristic of fraction_ring Jun 6, 2021
@bors bors bot closed this Jun 6, 2021
@bors bors bot deleted the char_p_localization branch June 6, 2021 08:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ericrbg ericrbg ericrbg left review comments

@eric-wieser eric-wieser eric-wieser approved these changes

@semorrison semorrison Awaiting requested review from semorrison

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
4 participants
@joneugster @semorrison @eric-wieser @ericrbg