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.

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

[Merged by Bors] - feat: dividing an element of a euclidean domain by its radical #18449

Closed
wants to merge 8 commits into from

Conversation

seewoo5
Copy link
Collaborator

@seewoo5 seewoo5 commented Oct 30, 2024

For a in a EuclideanDomain, define divRadical a as a / radical a


Prove some related theorems.
This is needed in the proof of Mason-Stothers theorem, and also a part of PR #15706.

Open in Gitpod

Copy link

github-actions bot commented Oct 30, 2024

PR summary 6105ab90ff

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.RingTheory.Radical 1081 1083 +2 (+0.19%)
Import changes for all files
Files Import difference
Mathlib.RingTheory.Radical 2

Declarations diff

+ _root_.IsCoprime.divRadical
+ divRadical
+ divRadical_dvd_self
+ divRadical_isUnit
+ divRadical_mul
+ divRadical_mul_radical
+ divRadical_ne_zero
+ eq_divRadical
+ radical_mul_divRadical

You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Oct 30, 2024
@seewoo5 seewoo5 mentioned this pull request Oct 30, 2024
1 task
@YaelDillies YaelDillies changed the title divRadical for euclidean domain feat: dividing an element of a euclidean domain by its radical Oct 30, 2024
Mathlib/RingTheory/Radical.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/Radical.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/Radical.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/Radical.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/Radical.lean Outdated Show resolved Hide resolved
@seewoo5 seewoo5 self-assigned this Oct 30, 2024
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

maintainer merge

apart from that. Thanks!

Mathlib/RingTheory/Radical.lean Outdated Show resolved Hide resolved
Copy link

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

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.

Thanks!

bors d+

theorem divRadical_dvd_self (a : E) : divRadical a ∣ a := by
exact Dvd.intro (radical a) (divRadical_mul_radical a)

protected theorem IsCoprime.divRadical {a b : E} (h : IsCoprime a b) :
Copy link
Member

Choose a reason for hiding this comment

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

What about calling this _root_.IsCoprime.divRadical?

Copy link
Collaborator Author

@seewoo5 seewoo5 Oct 31, 2024

Choose a reason for hiding this comment

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

Honestly, I don't know which one would be better (protected vs _root_), could you elaborate more? Someone in Discord explained about the differences, and it seems that _root_ is the better choice for this case. Thanks!

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Oct 31, 2024

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

@seewoo5
Copy link
Collaborator Author

seewoo5 commented Oct 31, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Oct 31, 2024
For `a` in a `EuclideanDomain`, define `divRadical a` as `a / radical a`



Co-authored-by: Seewoo Lee <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Oct 31, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: dividing an element of a euclidean domain by its radical [Merged by Bors] - feat: dividing an element of a euclidean domain by its radical Oct 31, 2024
@mathlib-bors mathlib-bors bot closed this Oct 31, 2024
@mathlib-bors mathlib-bors bot deleted the feature/divradical-ed branch October 31, 2024 18:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
delegated maintainer-merge t-algebra Algebra (groups, rings, fields, etc)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants