[Merged by Bors] - feat(RingTheory/Radical): Theorems for coprime elements + alpha by seewoo5 · Pull Request #15331 · leanprover-community/mathlib4

seewoo5 · 2024-07-30T16:48:47Z

More theorems on element radical, especially multiplicativity of radical for coprime elements.

depends on: [Merged by Bors] - feat(RingTheory/Radical): Radical of an element in a unique factorization normalization monoid #14873
depends on: [Merged by Bors] - refactor: Restrict scope of radical to UniqueFactorizationDomain #15826
depends on: [Merged by Bors] - Fix typo of author name #15818

github-actions · 2024-07-30T16:49:31Z

PR summary 024a80ca52

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ disjoint_normalizedFactors
+ disjoint_primeFactors
+ mul_primeFactors_disjUnion
+ radical_mul
+ radical_ne_zero
+ radical_neg
+ radical_neg_one

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.

Mathlib/RingTheory/Radical.lean

seewoo5 · 2024-07-30T17:25:37Z

@erdOne Thank you for the reviews! It seems that most of them are for #14873. Could you leave the comments there? Then I'll updated in that PR accordingly.

…oprime

Mathlib/RingTheory/Radical.lean

Ruben-VandeVelde · 2024-09-11T14:59:02Z

Mathlib/RingTheory/Radical.lean

+-- Theorems for commutative rings
+
+-- TODO: This holds for "nontrivial" monoids - do not need ring assumption.
+theorem radical_ne_zero (a : R) : radical a ≠ 0 := by


Yes, please state it in the generality that works.

Mathlib/RingTheory/Radical.lean

Ruben-VandeVelde · 2024-09-11T15:03:17Z

Mathlib/RingTheory/Radical.lean

+  rw [Finset.prod_disjUnion (disjoint_primeFactors hc)]
+
+theorem radical_neg {a : R} : radical (-a) = radical a :=
+  neg_one_mul a ▸ (radical_eq_of_associated <| associated_unit_mul_left a (-1) isUnit_one.neg)


I thought I added a lemma that a and -a are associated at some point. Can you please look for it?

I'm looking at Algebra.Associated.Basic now, and I can find neg_left or neg_right which can be used combined with rfl, but not exactly something like Associated (-a) a. Should I look for different file?

radical_eq_of_associated (.neg_right .rfl) (or some thing similar; not tested) is still shorter than this though.

@erdOne Just updated - radical_eq_of_associated Associated.rfl.neg_left worked!

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

seewoo5 · 2024-10-14T21:22:55Z

@Ruben-VandeVelde Hi, let me know if there are anything that I may update, thanks!

Mathlib/RingTheory/Radical.lean

erdOne · 2024-10-17T13:28:58Z

Mathlib/RingTheory/Radical.lean

+  rw [Finset.prod_disjUnion (disjoint_primeFactors hc)]
+
+theorem radical_neg {a : R} : radical (-a) = radical a :=
+  neg_one_mul a ▸ (radical_eq_of_associated <| associated_unit_mul_left a (-1) isUnit_one.neg)


radical_eq_of_associated (.neg_right .rfl) (or some thing similar; not tested) is still shorter than this though.

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

…er-community/mathlib4 into feature/element-radical-coprime

jcommelin

bors d+

Mathlib/RingTheory/Radical.lean

mathlib-bors · 2024-10-26T14:39:53Z

✌️ 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.

Co-authored-by: Johan Commelin <johan@commelin.net>

seewoo5 · 2024-10-26T17:47:08Z

bors r+

Co-authored-by: Jineon Baek <jcpaik@jcpaik-desktop.local> Co-authored-by: Seewoo Lee <49933279+seewoo5@users.noreply.github.com>

mathlib-bors · 2024-10-26T17:54:51Z

Pull request successfully merged into master.

Build succeeded:

seewoo5 and others added 8 commits July 18, 2024 09:28

initial commit

e270cb8

remove unnecessary import

b172681

lint

b542624

mathlib.lean

0a9d1af

edit comments

fbb690d

Name changes + edit comments

188206f

Add simp tag

d148c69

theorems for coprime elements

826ce60

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jul 30, 2024

seewoo5 added t-algebra Algebra (groups, rings, fields, etc) and removed new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! labels Jul 30, 2024

seewoo5 self-assigned this Jul 30, 2024

erdOne reviewed Jul 30, 2024

View reviewed changes

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

erdOne reviewed Jul 30, 2024

View reviewed changes

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

erdOne reviewed Jul 30, 2024

View reviewed changes

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

erdOne reviewed Jul 30, 2024

View reviewed changes

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

erdOne reviewed Jul 30, 2024

View reviewed changes

Mathlib/RingTheory/Radical.lean Show resolved Hide resolved

ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 30, 2024

address comments

0df94d7

seewoo5 mentioned this pull request Jul 30, 2024

[Merged by Bors] - feat(RingTheory/Radical): Radical of an element in a unique factorization normalization monoid #14873

Closed

seewoo5 added 5 commits July 30, 2024 13:09

rename alpha -> M

20840c1

minor

c20c796

merge & remove private

5e8f433

remove k

c1da6cd

Merge branch 'feature/element-radical' into feature/element-radical-c…

b7c8561

…oprime

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Aug 5, 2024

This was referenced Aug 5, 2024

Porting Radical.lean seewoo5/lean-poly-abc#48

Closed

[Merged by Bors] - feat: Mason-Stothers theorem (polynomial ABC) #15706

Closed

Ruben-VandeVelde reviewed Aug 31, 2024

View reviewed changes

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

hMul -> mul

b989fd6

Ruben-VandeVelde approved these changes Sep 11, 2024

View reviewed changes

Ruben-VandeVelde added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 11, 2024

seewoo5 and others added 3 commits September 12, 2024 09:38

Apply suggestions from code review

0d830b5

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

MulZeroClass.mul_zero -> mul_zero

583d418

upgrade radical_ne_zero to Nontrivial monoid

ec70630

seewoo5 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 7, 2024

erdOne reviewed Oct 17, 2024

View reviewed changes

erdOne added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 17, 2024

seewoo5 and others added 7 commits October 19, 2024 11:32

lint

83b2c05

Update Mathlib/RingTheory/Radical.lean

4d8c587

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

separate namespace

8bcb5b9

Merge branch 'feature/element-radical-coprime' of github.com:leanprov…

264bf6e

…er-community/mathlib4 into feature/element-radical-coprime

Merge branch 'master' into feature/element-radical-coprime

0487c0b

make radical_neg shorter

a201b08

remove by exact

f20fc5f

seewoo5 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 19, 2024

jcommelin reviewed Oct 26, 2024

View reviewed changes

Mathlib/RingTheory/Radical.lean Show resolved Hide resolved

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Oct 26, 2024

seewoo5 and others added 2 commits October 26, 2024 09:47

Update Mathlib/RingTheory/Radical.lean

3080482

Co-authored-by: Johan Commelin <johan@commelin.net>

remove back

024a80c

mathlib-bors bot pushed a commit that referenced this pull request Oct 26, 2024

feat(RingTheory/Radical): Theorems for coprime elements + alpha (#15331)

8102abc

Co-authored-by: Jineon Baek <jcpaik@jcpaik-desktop.local> Co-authored-by: Seewoo Lee <49933279+seewoo5@users.noreply.github.com>

mathlib-bors bot changed the title ~~feat(RingTheory/Radical): Theorems for coprime elements + alpha~~ [Merged by Bors] - feat(RingTheory/Radical): Theorems for coprime elements + alpha Oct 26, 2024

mathlib-bors bot closed this Oct 26, 2024

mathlib-bors bot deleted the feature/element-radical-coprime branch October 26, 2024 17:54

Conversation

seewoo5 commented Jul 30, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jul 30, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 024a80ca52

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

seewoo5 commented Jul 30, 2024

Uh oh!

Uh oh!

Uh oh!

Ruben-VandeVelde Sep 11, 2024

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Ruben-VandeVelde Sep 11, 2024

Choose a reason for hiding this comment

Uh oh!

seewoo5 Sep 12, 2024

Choose a reason for hiding this comment

Uh oh!

erdOne Oct 17, 2024

Choose a reason for hiding this comment

Uh oh!

seewoo5 Oct 19, 2024

Choose a reason for hiding this comment

Uh oh!

seewoo5 commented Oct 14, 2024

Uh oh!

Uh oh!

Uh oh!

Uh oh!

erdOne Oct 17, 2024

Choose a reason for hiding this comment

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mathlib-bors bot commented Oct 26, 2024

Uh oh!

seewoo5 commented Oct 26, 2024

Uh oh!

mathlib-bors bot commented Oct 26, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

seewoo5 commented Jul 30, 2024 •

edited

Loading

github-actions bot commented Jul 30, 2024 •

edited

Loading