[Merged by Bors] - feat: dividing an element of a euclidean domain by its radical #18449
Conversation
PR summary 6105ab90ff
|
| 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.
YaelDillies
changed the title
divRadical for euclidean domain
Co-authored-by: Yaël Dillies <[email protected]>
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
Co-authored-by: Yaël Dillies <[email protected]>
Mathlib/RingTheory/Radical.lean
Outdated
| 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) : |
There was a problem hiding this comment.
What about calling this _root_.IsCoprime.divRadical?
There was a problem hiding this comment.
Honestly, I don't know which one would be better ( Someone in Discord explained about the differences, and it seems that protected vs _root_), could you elaborate more?_root_ is the better choice for this case. Thanks!
|
✌️ seewoo5 can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
For `a` in a `EuclideanDomain`, define `divRadical a` as `a / radical a` Co-authored-by: Seewoo Lee <[email protected]>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
For
ain aEuclideanDomain, definedivRadical aasa / radical aProve some related theorems.
This is needed in the proof of Mason-Stothers theorem, and also a part of PR #15706.