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/ideal/operations.lean): lemmas about coprime ideals #14176

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(ring_theory/ideal/operations.lean): lemmas about coprime ideals #14176

wants to merge 5 commits into from

Conversation

pbazin
Copy link
Collaborator

@pbazin pbazin commented May 16, 2022

Generalises some lemmas from ring_theory/coprime/lemmas.lean to the case of non-principal ideals.

Open in Gitpod

@pbazin pbazin mentioned this pull request May 16, 2022
Closed
3 tasks
@pbazin pbazin added the awaiting-review The author would like community review of the PR label May 16, 2022
riccardobrasca
riccardobrasca approved these changes May 18, 2022
View reviewed changes
Copy link
Member

@riccardobrasca riccardobrasca left a comment

Choose a reason for hiding this comment

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

Do you think it is possible to extract some sublemmas from the proof?

src/ring_theory/coprime/ideal.lean Outdated Show resolved Hide resolved
@pbazin
Copy link
Collaborator Author

pbazin commented May 18, 2022

Do you think it is possible to extract some sublemmas from the proof?

The proofs of both directions of the iff could be separated in two lemmas but otherwise not

@riccardobrasca
Copy link
Member

Thanks!

bors d+

@bors
Copy link

bors bot commented May 18, 2022

✌️ pbazin can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels May 18, 2022
@pbazin
Copy link
Collaborator Author

pbazin commented May 18, 2022

bors r+

bors bot pushed a commit that referenced this pull request May 18, 2022
@pbazin
feat(ring_theory/ideal/operations.lean): lemmas about coprime ideals (#…
cfedf1d 
…14176)

Generalises some lemmas from `ring_theory/coprime/lemmas.lean` to the case of non-principal ideals.
@bors
Copy link

bors bot commented May 18, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(ring_theory/ideal/operations.lean): lemmas about coprime ideals [Merged by Bors] - feat(ring_theory/ideal/operations.lean): lemmas about coprime ideals May 18, 2022
@bors bors bot closed this May 18, 2022
@bors bors bot deleted the coprime_ideals branch May 18, 2022 16:03
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
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@pbazin @riccardobrasca