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(ring_theory/dedekind_domain/ideal): construct map between the sets of prime factors of ideal I and J induced by an isomorphism between R/I and S/J #16455

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - feat(ring_theory/dedekind_domain/ideal): construct map between the sets of prime factors of ideal I and J induced by an isomorphism between R/I and S/J #16455

wants to merge 8 commits into from

Conversation

Paul-Lez
Copy link
Collaborator

These lemmas generalize results that were originally in #15000.

Co-authored-by: Anne Baanen vierkantor@vierkantor.com

Open in Gitpod

@Paul-Lez Paul-Lez added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels Sep 10, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Sep 10, 2022
@riccardobrasca riccardobrasca self-assigned this Sep 10, 2022
@Paul-Lez Paul-Lez added the t-algebra Algebra (groups, rings, fields etc) label Sep 11, 2022
riccardobrasca
riccardobrasca approved these changes Sep 12, 2022
View reviewed changes
src/ring_theory/dedekind_domain/ideal.lean Outdated Show resolved Hide resolved
src/ring_theory/dedekind_domain/ideal.lean Show resolved Hide resolved
@riccardobrasca
Copy link
Member

Thanks!

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 Sep 12, 2022
bors bot pushed a commit that referenced this pull request Sep 12, 2022
@Paul-Lez @Vierkantor
feat(ring_theory/dedekind_domain/ideal): construct map between the se…
36e0130 
…ts of prime factors of ideal `I` and `J` induced by an isomorphism between `R/I` and `S/J` (#16455)

These lemmas generalize results that were originally in #15000.

Co-authored-by: Anne Baanen  <vierkantor@vierkantor.com>
@bors
Copy link

bors bot commented Sep 12, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(ring_theory/dedekind_domain/ideal): construct map between the sets of prime factors of ideal I and J induced by an isomorphism between R/I and S/J [Merged by Bors] - feat(ring_theory/dedekind_domain/ideal): construct map between the sets of prime factors of ideal I and J induced by an isomorphism between R/I and S/J Sep 12, 2022
@bors bors bot closed this Sep 12, 2022
@bors bors bot deleted the dedekind_domain_commit branch September 12, 2022 21:06
bottine pushed a commit that referenced this pull request Sep 13, 2022
@Paul-Lez @Vierkantor @bottine
feat(ring_theory/dedekind_domain/ideal): construct map between the se…
98b10cf 
…ts of prime factors of ideal `I` and `J` induced by an isomorphism between `R/I` and `S/J` (#16455)

These lemmas generalize results that were originally in #15000.

Co-authored-by: Anne Baanen  <vierkantor@vierkantor.com>
b-mehta pushed a commit that referenced this pull request Sep 21, 2022
@Paul-Lez @Vierkantor @b-mehta
feat(ring_theory/dedekind_domain/ideal): construct map between the se…
87770b9 
…ts of prime factors of ideal `I` and `J` induced by an isomorphism between `R/I` and `S/J` (#16455)

These lemmas generalize results that were originally in #15000.

Co-authored-by: Anne Baanen  <vierkantor@vierkantor.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@riccardobrasca riccardobrasca riccardobrasca approved these changes

Assignees

@riccardobrasca riccardobrasca

Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-algebra Algebra (groups, rings, fields etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@Paul-Lez @riccardobrasca