Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(ring_theory.integral_domain): add exists_eq_pow_of_mul_eq_pow_of_coprime#17877

Closed
riccardobrasca wants to merge 9 commits intomasterfrom
RB/exists_eq_pow_of_mul_eq_pow
Closed

[Merged by Bors] - feat(ring_theory.integral_domain): add exists_eq_pow_of_mul_eq_pow_of_coprime#17877
riccardobrasca wants to merge 9 commits intomasterfrom
RB/exists_eq_pow_of_mul_eq_pow

Conversation

@riccardobrasca
Copy link
Copy Markdown
Member

@riccardobrasca riccardobrasca commented Dec 9, 2022 •
edited
Loading

We add exists_eq_pow_of_mul_eq_pow_of_coprime: this is done for semirings, in order to apply to ideal R for a Dedekind domain R.

Corresponding mathlib4 PR #928.

Open in Gitpod

@riccardobrasca riccardobrasca added awaiting-review The author would like community review of the PR t-algebra Algebra (groups, rings, fields etc) modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. labels Dec 9, 2022
@riccardobrasca riccardobrasca mentioned this pull request Dec 9, 2022
Closed
jcommelin
jcommelin approved these changes Dec 10, 2022
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-bot-assistant leanprover-community-bot-assistant 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 Dec 10, 2022
bors bot pushed a commit that referenced this pull request Dec 10, 2022
@riccardobrasca
feat(ring_theory.integral_domain): add exists_eq_pow_of_mul_eq_pow_of…
12d63a7 
…_coprime (#17877)

We add `exists_eq_pow_of_mul_eq_pow_of_coprime`: this is done for semirings, in order to apply to `ideal R` for a Dedekind domain `R`.

Corresponding mathlib4 PR [#928](leanprover-community/mathlib4#928).
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 10, 2022
@riccardobrasca
chore: generalize IsDomain.toCancelCommMonoidWithZero to semirings (#928
ce207d1 
)

Corresponding mathlib3 PR: [#17877](leanprover-community/mathlib3#17877).
@bors
Copy link
Copy Markdown

bors bot commented Dec 10, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(ring_theory.integral_domain): add exists_eq_pow_of_mul_eq_pow_of_coprime [Merged by Bors] - feat(ring_theory.integral_domain): add exists_eq_pow_of_mul_eq_pow_of_coprime Dec 10, 2022
@bors bors bot closed this Dec 10, 2022
@bors bors bot deleted the RB/exists_eq_pow_of_mul_eq_pow branch December 10, 2022 16:28
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

1 more reviewer

@jcommelin jcommelin jcommelin approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. 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.

3 participants

@riccardobrasca @jcommelin @leanprover-community-bot-assistant